proposition: Lemma big_tcast n m (n_m : n = m) (A : finType) F (P : pred {: n.-tuple A}) : \big[op/idx]_(p in {: n.-tuple A} | P p) F p = \big[op/idx]_(p in {: m.-tuple A} | P (tcast (esym n_m) p)) F (tcast (esym n_m) p).
proof: Proof. subst m; apply eq_bigr => ta => /andP[_ H]; by rewrite tcast_id. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext