proposition: Lemma big_rV0_row_of_tuple f (P : pred _) : \big[M/idx]_(v in 'rV[A]_0 | P v) f v = if P (row_of_tuple [tuple]) then f (row_of_tuple [tuple]) else idx.
proof: Proof. rewrite -big_map /= /index_enum -enumT /=. set e := enum _. rewrite (_ : e = [:: row_of_tuple [tuple]]). by rewrite /= big_cons big_nil Monoid.addm0. rewrite /e. apply (@eq_from_nth _ (row_of_tuple [tuple])). by rewrite -cardE card_mx muln0 expn0. move=> i. rewrite -cardE card_mx muln0 expn0 ltnS leqn0 => /eqP ->{i}. rewrite -/e. destruct e => //. apply val_inj => /=. by apply/ffunP => /= -[? []]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext