{R : Ring} x `{!IsInvertible R x} : left_inverse_elem x = right_inverse_elem x. Proof. nrapply (path_left_right_inverse x). - apply left_inverse_eq. - apply right_inverse_eq. 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.