proposition: Theorem update_primes_true_imp_div : forall (k:nat)(l: list (nat*nat)), all_first_less_than k l -> all_multiples l -> all_greater_than_one l -> forall l1, update_primes k l = (l1, true) -> (exists p:nat, 1< p < k /\ (exists q:nat, k = p*q)).
proof: Proof. intros k l; elim l. - simpl; intros; discriminate. - intros (p,n) l0 Hrec Haf Ham Hal l1; simpl. case_eq (update_primes k l0). intros l2 b Hup; case_eq (Nat.compare k n). + intros Htwc Heq; generalize (nat_compare_eq _ _ Htwc). intros Hk; exists p; split. * split. unfold all_greater_than_one in Hal; apply Hal with (nil (A:=nat*nat)) l0 n; auto. unfold all_first_less_than in Haf; apply Haf with (nil (A:=nat*nat)) l0 n; auto. * unfold all_multiples in Ham. rewrite Hk; apply Ham with (nil (A:=nat*nat)) l0; auto. + intros Htwc Heq; injection Heq; intros Hb Hl1. * rewrite Hb in Hup; apply Hrec with l2. -- apply all_first_less_than_transmit with (p,n); auto. -- apply all_multiples_transmit with (p,n); auto. -- apply all_greater_than_one_transmit with (p,n); auto. -- auto. + intros Htwc Heq; injection Heq; intros Hb Hl1. rewrite Hb in Hup; apply Hrec with l2. * apply all_first_less_than_transmit with (p,n); auto. * apply all_multiples_transmit with (p,n); auto. * apply all_greater_than_one_transmit with (p,n); auto. * auto. Qed.
imports: List Arith