Lemma prime_ideal_ax1_contraposition : ∀ a b : R, ¬ p a ⇒ ¬ p b ⇒ ¬ p (a * b). Proof. intros a b Ha Hb. apply (negf (prime_ideal_ax1 p a b)), toneghdisj. exact (make_dirprod Ha Hb). Qed.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.