proposition: Lemma big_rV_belast_last n (F : 'rV[A]_n.+1 -> R) (P1 : pred 'rV[A]_n) (P2 : pred A) : \big[M/idx]_(i in 'rV[A]_n | P1 i) \big[M/idx]_(j in A | P2 j) (F (castmx (erefl, addn1 n) (row_mx i (\row_(k < 1) j)))) = \big[M/idx]_(p in 'rV[A]_n.+1 | (P1 (rbelast p)) && (P2 (rlast p)) ) (F p).
proof: Proof. rewrite [in RHS](partition_big (fun x : 'rV_n.+1 => rlast x) P2) /=; last first. by move=> i /andP[]. rewrite exchange_big. apply eq_bigr => i Hi. rewrite (reindex_onto (fun j => (castmx (erefl 1%nat, addn1 n) (row_mx j (\row_(k < 1) i)))) rbelast) /=; last first. move=> j /andP[] Hj1 /eqP => <-; by rewrite row_mx_rbelast. apply eq_big => //= x. by rewrite row_mx_row_ord_max rbelast_row_mx 2!eqxx !andbT Hi andbT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext