proposition: Theorem update_primes_all_multiples : forall k l l' b, all_multiples l -> update_primes k l = (l', b) -> all_multiples l'.
proof: Proof. apply (update_primes_all_list_invariant (fun k p n => exists q:nat, n=p*q)); try (intros k p n Hcomp (q, Heq);exists (S q);rewrite Heq; rewrite <- mult_n_Sm; reflexivity). Qed.
imports: List Arith