proposition: Lemma big_cast_rV n m (n_m : n = m) (A : finType) F (P : pred {: 'rV[A]_n}) : \big[op/idx]_(p in {: 'rV_n} | P p) F p = \big[op/idx]_(p in {: 'rV_m} | P (castmx (erefl, esym n_m) p)) F (castmx (erefl, esym n_m) p).
proof: Proof. by subst m; apply eq_bigr => ta => /andP[_ H]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext