Lemma azerorelcomp ( cd : A × aintdomazerosubmonoid A ) ( ef : A × aintdomazerosubmonoid A ) ( p : pr1 cd * pr1 ( pr2 ef ) = pr1 ef * pr1 ( pr2 cd ) ) ( q : pr1 cd # 0 ) : pr1 ef # 0. Proof. intros. change ( @op2 A ( pr1 cd ) ( pr1 ( pr2 ef ) ) = @op2 A ( pr1 ef ) ( pr1 ( pr2 cd ) ) ) in p. assert ( ( @op2 A ( pr1 cd ) ( pr1 ( pr2 ef ) ) ) # 0 ) as v. { apply A. - assumption. - apply ( pr2 ( pr2 ef ) ). } rewrite p in v. apply ( pr1 ( timesazero v ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields.