proposition: Theorem update_primes_all_first_prime : forall k l l' b, all_first_prime l -> update_primes k l = (l',b) -> all_first_prime l'.
proof: Proof. apply (update_primes_all_list_invariant (fun k p n => prime p)); auto. Qed.
imports: List Arith