proposition: Lemma big_setX (a : {set A}) (b : {set B}) f : \big[M/idx]_(x in a `* b) f x = \big[M/idx]_(x in a) \big[M/idx]_(y in b) f (x, y).
proof: Proof. rewrite (eq_bigl (fun x => (x.1 \in a) && (x.2 \in b))); last first. by case=> x y; rewrite in_setX. rewrite (eq_bigr (fun x => f (x.1, x.2))); last by case. by rewrite -(pair_big _ _ (fun a b => f (a, b))). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext