proposition: Lemma cnvarsym_leq_trans m n p : (m <= n) -> (n <= p) -> @cnvarsym R n p \o @cnvarsym R m n =1 @cnvarsym R m p.
proof: Proof. move=> le_m_n le_n_p f; rewrite -(sympolyfK f) /=. move: (sympolyf f) => {}f; rewrite (mpolyE f) !raddf_sum /=. apply eq_bigr => x _; rewrite !mulr_algl !linearZ /=; congr (_ *: _). rewrite (multinomUE_id x) !rmorph_prod /=. apply eq_bigr => i _; rewrite !rmorphXn /= !cnvar_leq_symeE //. by rewrite ltnS (leq_trans _ le_m_n) // -ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv