{R : Ring} (x : R) `{IsInvertible R x} : x * inverse_elem x = 1. Proof. rhs_V nrapply (right_inverse_eq x). f_ap. apply path_left_inverse_elem_right_inverse_elem. 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.