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