proposition: Lemma big_rV_1 f g (P : pred _) (Q : pred _): (forall i : 'rV[A]_1, f i = g (i ``_ ord0)) -> (forall i : 'rV[A]_1, P i = Q (i ``_ ord0)) -> \big[M/idx]_(i in 'rV[A]_1 | P i) f i = \big[M/idx]_(i in A | Q i) g i.
proof: Proof. move=> FG PQ. rewrite (reindex_onto (fun i => \row_(j < 1) i) (fun p => p ``_ ord0)) /=; last first. move=> m Pm. apply/rowP => a; by rewrite {a}(ord1 a) mxE. apply eq_big => a. by rewrite PQ mxE eqxx andbT. by rewrite FG !mxE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext