fact: Fixpoint mProd (A B C : Set) (l1 : list A) (l2 : list B) {struct l2} : list (A * B) := match l2 with | nil => nil | b :: l2' => map (fun a : A => (a, b)) l1 ++ mProd A B C l1 l2' end.
imports: Reals ZArith List PeanoNat Psatz