proposition: Lemma big_rV_cons_behead n (F : 'rV[A]_n.+1 -> R) (P1 : pred A) (P2 : pred 'rV[A]_n) : \big[M/idx]_(i in A | P1 i) \big[M/idx]_(j in 'rV[A]_n | P2 j) (F (row_mx (\row_(k < 1) i) j)) = \big[M/idx]_(p in 'rV[A]_n.+1 | (P1 (p ``_ ord0)) && (P2 (rbehead p)) ) (F p).
proof: Proof. rewrite [in RHS](partition_big (fun x : 'rV_n.+1 => x ``_ ord0) P1) /=; last first. by move=> i /andP[]. apply eq_bigr => i Hi. rewrite (reindex_onto (fun j => row_mx (\row_(k < 1) i) j) rbehead) /=; last first. move=> j /andP[] Hj1 /eqP => <-; by rewrite row_mx_rbehead. apply eq_big => //= x; by rewrite row_mx_row_ord0 rbehead_row_mx 2!eqxx Hi !andbT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext