proposition: Lemma in_prod_aux : forall (x:A) (y:B) (l:list B), In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
proof: Proof. intros x y l; induction l; [ simpl; auto | simpl; destruct 1 as [H1| ]; [ left; rewrite H1; trivial | right; auto ] ]. Qed.
imports: PeanoNat