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