proposition: Theorem all_multiples_add : forall l n p, (exists q:nat, n=p*q)-> all_multiples l -> all_multiples ((p,n)::l).
proof: Proof. intros l n p Hdiv Ham l1; case l1. - simpl; intros l2 p' n' Heq; injection Heq; intros Hl2 Hn' Hp'; rewrite <- Hn'; rewrite <- Hp'; assumption. - clear l1; simpl; intros fst_elem l1 l2 p' n' Heq; injection Heq; intros Hl Hfst; apply (Ham l1 l2); assumption. Qed.
imports: List Arith