proposition: Lemma ringminusminus (X : ring) (a : X) : --a = a.
proof: Proof. intros. apply (grinvinv X a). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids