proposition: Lemma big_rV1_ord0 (f : A -> R) k : \big[M/idx]_(i in A) f i = k -> \big[M/idx]_(i in 'rV[A]_1) f (i ``_ ord0) = k.
proof: Proof. move=> <-. rewrite (reindex_onto (fun j => \row_(i < 1) j) (fun p => p ``_ ord0)) /=. - apply eq_big => a; first by rewrite mxE eqxx inE. move=> _; by rewrite mxE. - move=> t _; apply/rowP => a; by rewrite (ord1 a) mxE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext