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