proposition: Theorem update_primes_all_intervals : forall (k:nat)(l:list(nat*nat)), all_intervals k l -> all_greater_than_one l -> forall l' b, update_primes k l = (l',b) -> all_intervals (S k) l'.
proof: Proof. intros k l; elim l. - simpl; intros Hai Hal l' b Hup; injection Hup; intros Hb Hl'; rewrite <- Hl'. intros l1 l2 n p Heq; elim (absurd_decompose_list _ _ _ _ Heq). - simpl; intros (p, n) l0 Hrec Hai Hal l' b; case_eq (update_primes k l0); intros l'0 b0 Hup0 Hup l1. case l1. + unfold all_intervals in Hai. case_eq (Nat.compare k n); simpl; intros Htwc l2 p' n' Heq; rewrite Htwc in Hup; injection Hup; intros Hb Hl'; rewrite <- Hl' in Heq; injection Heq; intros Hl2 Hn' Hp'; rewrite <- Hp'; rewrite <- Hn'; generalize (Hai nil l0 p n (refl_equal _)); intros (Hlt, Hle);split; (generalize (nat_compare_Lt_lt _ _ Htwc) || generalize (nat_compare_eq _ _ Htwc) || generalize (nat_compare_Gt_gt _ _ Htwc)); auto with arith. * intros Heq2; rewrite Heq2; rewrite Nat.add_sub; auto with arith. * intros Heq2; rewrite Heq2; unfold all_greater_than_one in Hal; generalize (Hal nil l0 p n (refl_equal _)); intros Hpgt1. pattern n at 1; rewrite plus_n_O; rewrite plus_n_Sm; apply Nat.add_le_mono; auto with arith. * rewrite Nat.add_sub; auto with arith. * generalize (Hal nil l0 p n (refl_equal _)); intros Hpgt1. intros Hkltn; pattern k at 1; rewrite plus_n_O; rewrite plus_n_Sm; apply Nat.add_le_mono; auto with arith. + generalize (all_intervals_transmit _ _ _ Hai); intros Hai'. generalize (all_greater_than_one_transmit _ _ Hal); intros Hal'. simpl; clear l1; intros fst_elem l1 l2 p' n' Heq; generalize Hup; rewrite Heq. case (Nat.compare k n); intros Hup'; injection Hup'; intros Hb Hl' _; apply (Hrec Hai' Hal' l'0 b0 Hup0 l1 l2); assumption. Qed.
imports: List Arith