proposition: Lemma cast_permE m n (eq_m_n : m = n) (s : 'S_m) (i : 'I_n) : cast_perm eq_m_n s i = cast_ord eq_m_n (s (cast_ord (esym eq_m_n) i)).
proof: Proof. by rewrite cast_ord_permE cast_ordKV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)