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