proposition: Lemma cartesian_product_filters {A B} (f : A -> bool) (g : B -> bool) xs ys : cartesian_product (filter f xs) (filter g ys) = filter (fun p => andb (f (fst p)) (g (snd p))) (cartesian_product xs ys).
proof: Proof. revert ys. induction xs; intros ys; auto. simpl. rewrite filter_app. rewrite <-IHxs. destruct (f a) eqn:Ha. - simpl. f_equal. clear -Ha. induction ys as [| b ys IHys]; auto. simpl. destruct (f a), (g b); simpl; congruence. - rewrite IHxs. match goal with |- ?a = _ => transitivity ([] ++ a) end. reflexivity. f_equal. induction ys as [| b ys IHys]; auto. simpl. destruct (f a), (g b); simpl; try congruence. Qed.
imports: Arith ZArith List Lia