Lemma ringrmultminus (X : ring) (a b : X) : a * -b = -(a * b). Proof. intros. apply (@grrcan X _ _ (a * b)). change (a * (- b) + a * b = - (a * b) + a * b). rewrite (ringlinvax1 X _). rewrite <- (ringldistr X _ _ _). rewrite (ringlinvax1 X _). rewrite (ringmultx0 X _). apply idpath. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.