proposition: Lemma azerolmultcomp { a b c : A } ( p : a # 0 ) ( q : b # c ) : a * b # a * c.
proof: Proof. intros. apply aminuszeroa. rewrite <- ringminusdistr. apply ( pr2 A ). - assumption. - apply aaminuszero. assumption. Defined.
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields