proposition: Lemma Minvr t u : \sum_(v : T) (M t v) * (Minv v u) = (u == t)%:R.
proof: Proof. rewrite (reindex _ (onW_bij _ (@enum_val_bij _))) /=. transitivity (mulmx Mat (invmx Mat) (enum_rank t) (enum_rank u)). rewrite mxE; apply eq_bigr => /= i _. by rewrite /Minv mxE enum_valK enum_rankK. rewrite mulmxV; last by rewrite unitmxE det_unitrig unitr1. rewrite mxE; congr (nat_of_bool _)%:R. by apply/eqP/eqP => [/(can_inj (@enum_rankK _))|] ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)