proposition: Lemma in_prod : forall (l:list A) (l':list B) (x:A) (y:B), In x l -> In y l' -> In (x, y) (list_prod l l').
proof: Proof. intro l; induction l; [ simpl; tauto | simpl; intros l' x y H H0; apply in_or_app; destruct H as [H|H]; [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed.
imports: PeanoNat