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