{R : Ring} (x : R) (inv : R) (inv_l : inv * x = 1) (inv_r : x * inv = 1) : IsInvertible R x. Proof. split. - by exists inv. - unfold IsRightInvertible. by exists (inv : rng_op 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.