not_isprime_iff_iscomposite@{} n : 1 < n /\ ~ IsPrime n <-> IsComposite n. Proof. nrapply iff_compose. - nrapply iff_functor_prod. 1: nrapply iff_refl. nrapply iff_compose. + apply iff_not. rapply isprime_iff_not_iscomposite. + rapply iff_not_prod. - nrapply iff_compose. 1: nrapply sum_distrib_l. nrapply iff_compose. + nrapply iff_functor_sum. 1: apply iff_contradiction. nrapply iff_functor_prod. 1: nrapply iff_refl. rapply iff_stable. + nrapply iff_compose. 1: rapply sum_empty_l. split; only 1: exact snd. intros H; split; only 2: exact H. exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes