proposition: Lemma big_rV_behead n (F : 'rV[A]_n.+1 -> R) (w : 'rV[A]_n) : \big[M/idx]_(a in A) (F (row_mx (\row_(k < 1) a) w)) = \big[M/idx]_(v in 'rV[A]_n.+1 | rbehead v == w) (F v).
proof: Proof. rewrite [in RHS](reindex_onto (fun p => row_mx (\row_(k < 1) p) w) (fun p => p ``_ ord0) ) /=; last first. move=> i /eqP <-; by rewrite row_mx_rbehead. apply eq_bigl => ?; by rewrite rbehead_row_mx eqxx /= row_mx_row_ord0 eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext