Lemma ringlmultminus (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 <- (ringrdistr X _ _ _). rewrite (ringlinvax1 X _). rewrite (ringmult0x X _). apply idpath. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.