proposition: Theorem update_primes_true_aux : forall (k:nat) (l1 l2 l3 l4: list(nat*nat))(b:bool), update_primes k l1 = (l2, true) -> update_primes k (l3++l1) = (l4, b) -> b=true.
proof: Proof. intros k l1 l2 l3; elim l3. - simpl; intros l4 b Heq1; rewrite Heq1; intros Heq2; injection Heq2; auto. - simpl; intros (p,n) l; case (update_primes k (l++l1)). intros l4 b Hrec l4' b'; case (Nat.compare k n). + intros Heq1 Heq2; injection Heq2; auto. + intros Heq1 Heq2; injection Heq2. intros Heq3 Heq4; rewrite <- Heq3; apply Hrec with l4; auto. + intros Heq1 Heq2; injection Heq2. intros Heq3 Heq4; rewrite <- Heq3; apply Hrec with l4; auto. Qed.
imports: List Arith