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