{R : Ring} {x y : R} `{IsInvertible R x, IsInvertible R y} : x = y <~> inverse_elem x = inverse_elem y. Proof. srapply equiv_iff_hprop. - exact (isinvertible_unique x y). - exact (isinvertible_unique (inverse_elem x) (inverse_elem y)). 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.