proposition: Lemma azerormultcomp { a b c : A } ( p : a # 0 ) ( q : b # c ) : b * a # c * a.
proof: Proof. intros. rewrite ( @ringcomm2 A b ). rewrite ( @ringcomm2 A c ). apply ( azerolmultcomp p q ). Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields