proposition: Theorem update_primes_same_first : forall k l l' b, update_primes k l = (l', b) -> forall l1 l2 p n, l = l1++(p,n)::l2 -> (exists l'1 : list(nat*nat), (exists l'2 : list(nat*nat), (exists n': nat, l'=l'1++(p,n')::l'2))).
proof: Proof. intros k l; elim l. - intros l' b Hup l1 l2 p n Heq; elim (absurd_decompose_list _ _ _ _ Heq). - intros (p,n) l0 Hrec l' b. simpl; case_eq (update_primes k l0); intros l'0 b0 Hup'. case (Nat.compare k n); intros Hup; injection Hup; intros Hb Hl'; intros l1; (case l1; [simpl; intros l2 p0 n0 Heq; injection Heq; intros Hl2 Hn0 Hp0; rewrite <- Hl'; rewrite <- Hp0; exists (nil (A:=nat*nat)); exists l'0 | clear l1; simpl; intros fst_elem l1 l2 p0 n0 Heq; injection Heq; intros Hl0 Hfst_elem; rewrite <- Hl'; elim (Hrec l'0 b0 Hup' l1 l2 p0 n0 Hl0); intros l'1 (l'2, (n', Heq2)); rewrite Heq2]). + exists (n+p); reflexivity. + exists ((p,n+p)::l'1); exists l'2; exists n'; reflexivity. + exists n; reflexivity. + exists ((p,n)::l'1); exists l'2; exists n'; reflexivity. + exists (n+p); reflexivity. + exists ((p,n+p)::l'1); exists l'2; exists n'; reflexivity. Qed.
imports: List Arith