fact: Fixpoint cartesian_product {A B} (xs : list A) (ys : list B) : list (A * B) := match xs with | [] => [] | x :: xs => map (pair x) ys ++ cartesian_product xs ys end.
imports: Arith ZArith String List Psatz Factorial