proposition: Lemma pair_big_snd (F : {: A * B} -> R) P Q : P =1 Q \o snd -> \big[M/idx]_(i in A) \big[M/idx]_(j in B | Q j) F (i, j) = \big[M/idx]_(i in {: A * B} | P i) F i.
proof: Proof. move=> /= PQ; rewrite pair_big /=; apply eq_big; last by case. case=> /= ? ?; by rewrite PQ. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext