proposition: Theorem div_by_prime_aux : forall k:nat, forall n:nat, n <= k -> 1 < n -> (exists p:nat, 1 < p < n /\ (exists q : nat, n=p*q)) -> (exists p:nat, 1 < p < n /\ (prime p) /\ (exists q:nat, n=p*q)).
proof: Proof. intros k; elim k. - intros n Hle Hlt Hn. elim (Nat.lt_asymm 1 0). + apply Nat.lt_le_trans with n; assumption. + auto with arith. - intros k' Hrec n Hle Hlt Hn. elim (proj1 (Nat.lt_eq_cases n (S k')) Hle). + intros Hle'; apply Hrec; auto with arith. + elim Hn; intros p ((Hpgt1, Hpltn),(q,Heq)). intros HneqSk'. elim (prime_dec p). * intros Hpeq0or1; elim Hpeq0or1. -- intros Hpeq0. rewrite Hpeq0 in Hpgt1; elim (Nat.nlt_0_r 1); assumption. -- intros Hpeq1; rewrite Hpeq1 in Hpgt1; elim (Nat.lt_irrefl 1); assumption. * intros Hpdec; elim Hpdec. -- intros Hexp. elim (Hrec p); auto with arith. ++ intros p' ((Hp'gt1,Hp'ltp), (Hpr,(q', Heq'))). exists p'. split;[split|split]; auto with arith. ** apply Nat.lt_trans with p; auto with arith. ** exists (q' * q). rewrite Nat.mul_assoc. rewrite Heq; rewrite Heq'; trivial. ++ unfold lt in Hpltn. rewrite HneqSk' in Hpltn; auto with arith. -- exists p;split;[split|split]; auto with arith. exists q; auto with arith. Qed.
imports: List Arith