isprime_iff_not_iscomposite@{} n : IsPrime n <-> 1 < n /\ ~ IsComposite n. Proof. split. - intros H. split; only 1: exact _. intros [a [[H2 H3] H4]]. apply isprime in H4. destruct H4 as [H4|H4]; destruct H4; exact (lt_irrefl _ _). - intros [H1 H]. rapply Build_IsPrime. intros m d. destruct (dec (1 < d.1)) as [H2|H2]. + pose proof (divides_divisor _ _ d) as d'. apply leq_divides in d'. 2: exact _. apply equiv_leq_lt_or_eq in d'. destruct d' as [d'|d']. * assert (H' : IsComposite n). { exists d.1. split; only 1: split; exact _. } contradiction H. * destruct d as [d r]. simpl in *. destruct d'. left. rewrite <- nat_div_cancel with d. 2: exact _. rewrite <- nat_div_mul_cancel_l with d m. 2: exact _. by apply (ap (fun x => x / d)). + apply geq_iff_not_lt in H2. destruct d as [d r]. simpl in *; hnf in H2. destruct d. { rewrite nat_mul_zero_l in r. destruct n. 1: contradiction (not_lt_zero_r _ H1). contradiction (neq_nat_zero_succ _ r). } destruct d. { rewrite nat_mul_one_l in r. by right. } apply leq_pred' in H2. contradiction (not_lt_zero_r d). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes