Lemma timesazero { A : acommring } { a b : A } ( p : a * b # 0 ) : a # 0 × b # 0. 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.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.