proposition: Lemma ringmultminusminus (X : ring) (a b : X) : paths (-a * - b) (a * b).
proof: Proof. intros. apply (@grrcan X _ _ (- a * b)). simpl. rewrite (pathsinv0 (ringldistr X _ _ (- a))). rewrite (pathsinv0 (ringrdistr X _ _ b)). rewrite (ringlinvax1 X b). rewrite (ringrinvax1 X a). rewrite (ringmult0x X _). rewrite (ringmultx0 X _). apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids