(R : CRing) (x : R) (inv : R) (inv_l : inv * x = 1) : IsInvertible R x. Proof. snrapply Build_IsInvertible. - exact inv. - exact inv_l. - lhs nrapply rng_mult_comm. exact inv_l. Defined.
Require Import WildCat. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.AbGroups. Import Ideal.Notation.