proposition: Lemma length_cartesian_product {A B} (xs : list A) (ys : list B) : length (cartesian_product xs ys) = length xs * length ys.
proof: Proof. induction xs. reflexivity. simpl. rewrite app_length, map_length. congruence. Qed.
imports: Arith ZArith List Lia