proposition: Lemma cnvarsym_geq_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_n_m le_p_n 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 le_i_m]] _; rewrite !rmorphXn /=; congr (_ ^+ _). rewrite !(@cnvar_leq_symeE R m) //. case: (ltnP i n.+1) => [le_i_n1|lt_n_i]; first exact: cnvar_leq_symeE. rewrite !syme_geqnE ?raddf0 // ltnS. exact: (leq_ltn_trans le_p_n lt_n_i). 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