proposition: Lemma cast_perm_comp m n p (eq_m_n : m = n) (eq_n_p : n = p) s : cast_perm eq_n_p (cast_perm eq_m_n s) = cast_perm (etrans eq_m_n eq_n_p) s.
proof: Proof. by case: _ / eq_n_p. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)