{R : Ring} (x x' x'' : R) (p : x' * x = 1) (q : x * x'' = 1) : x' = x''. Proof. rhs_V nrapply rng_mult_one_l. rewrite <- p. rewrite <- simple_associativity. rewrite q. symmetry. apply rng_mult_one_r. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.