proposition: Theorem all_first_prime_add : forall (l:list(nat*nat))(p n:nat), prime p -> all_first_prime l -> all_first_prime ((p,n)::l).
proof: Proof. intros l p n Hlt Haf l1; case l1. - intros l2 p' n' Heq; injection Heq; intros Hl Hn' Hp'; rewrite <- Hp'; assumption. - simpl; clear l1; intros fst_elem l1 l2 p' n' Heq; injection Heq; intros Hl Hfst; apply (Haf l1 l2 p' n' Hl). Qed.
imports: List Arith