proposition: Theorem prime_dec_aux : forall n k:nat, (n=0\/n=1)\/ (exists p:nat, 1<p<k /\ (exists q:nat, n=p*q))\/ ((n<>0/\n<>1)/\~(exists p:nat, 1<p<k/\ (exists q:nat, n=p*q))).
proof: Proof. intros n; elim (eq_nat_or n 1). - auto. - intros Hnneq1. elim (eq_nat_or n 0). + auto. + intros Hnneq0 k; elim k. * right; right; split. -- auto. -- intros (p, ((_,Hlt0), (q, Heq))). elim (Nat.nlt_0_r p); auto. * intros k'; case k'. -- intros; right; right; split. ++ auto. ++ intros (p, ((Hpgt1, Hplt1),_)). elim (Nat.lt_irrefl 1); apply Nat.lt_trans with p;auto. -- intros k''; case k''. ++ intros; right; right; split; auto; intros (p, ((Hpgt1, Hplt2),_)). elim (Nat.lt_irrefl p); apply Nat.le_lt_trans with 1; auto with arith. ++ intros k''' Hrec; case (divides_dec_aux n n (S (S k'''))). ** auto with arith. ** intros Hdiv; right; left; exists (S (S k''')); repeat split; auto with arith. ** intros Hndiv; elim Hrec. { auto. } { intros Hrec'; elim Hrec'. intros (p, ((Hpgt1, Hplt), Hex)); right; left; exists p; repeat split; auto with arith. intros (_, Hnodiv); right; right; split; auto; intros (p, ((Hpgt1, Hplt), Hex)). assert (Hple : p <= S (S k''')). { auto with arith. } elim (proj1 (Nat.lt_eq_cases _ _) Hple). intros Hplt'. elim Hnodiv; exists p; repeat split; auto with arith. intros Hpeq. elim Hndiv; rewrite <- Hpeq; exact Hex. } Qed.
imports: List Arith