proposition: Lemma isom_cast_perm m n eq_m_n : isom setT setT (@cast_perm m n eq_m_n).
proof: Proof. case: {n} _ / eq_m_n; apply/isomP; split. exact/injmP/(in2W (@cast_perm_inj _ _ _)). by apply/setP => /= s /[!inE]; apply/imsetP; exists s; rewrite ?inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)