proposition: Lemma timesazero { A : acommring } { a b : A } ( p : a * b # 0 ) : a # 0 × b # 0.
proof: Proof. intros. split. - assert ( a * b # 0 * b ) as h. { rewrite ( ringmult0x A ). assumption. } apply ( pr2 ( acommring_amult A ) b ). assumption. - apply ( pr1 ( acommring_amult A ) a ). rewrite ( ringmultx0 A ). assumption. Defined.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids