proposition: Lemma cast_perm_sym m n (eq_m_n : m = n) s t : s = cast_perm eq_m_n t -> t = cast_perm (esym eq_m_n) s.
proof: Proof. by move/(canLR (cast_permK _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)