{R : Ring} (x : R) : {inv : R & prod (inv * x = 1) (x * inv = 1)} <~> IsInvertible R x. Proof. equiv_via { i : IsInvertible R x & right_inverse_elem x = left_inverse_elem x }. 1: make_equiv_contr_basedpaths. apply equiv_sigma_contr; intro i. rapply contr_inhabited_hprop. symmetry; 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.