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