{R : Ring} (x y : R) `{IsInvertible R x} `{IsInvertible R y} (p : x = y) : inverse_elem x = inverse_elem y. Proof. destruct p. snrapply (path_left_right_inverse x). - apply rng_inv_l. - apply rng_inv_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.