proposition: Lemma cnvar_symp i : (i < m) || (n <= m) -> cnvarsym 'p_i.+1 = 'p_i.+1.
proof: Proof. have [b/ltnW] := ubnP i; elim: b i => [| i IHi] d. rewrite leqn0 => /eqP -> H. by rewrite !sympe1E cnvar_syme. rewrite leq_eqVlt => /orP[/eqP ->{d} | ] Hi; last exact: IHi. have:= Newton_symh m0 R i.+2 => /(congr1 cnvarsym). rewrite linearZ /= cnvar_symh // Newton_symh. rewrite big_ltn // symh0 mul1r subn0 => /esym. rewrite linear_sum big_ltn //= rmorphM /= symh0 rmorph1 mul1r subn0. suff -> : \sum_(1 <= j < i.+2) cnvarsym ('h_j * 'p_(i.+2 - j)) = \sum_(1 <= j < i.+2) 'h_j * 'p_(i.+2 - j). by apply: addIr. rewrite !big_nat; apply eq_bigr => d /andP[H0d Hd]. rewrite rmorphM /= cnvar_symh; first last. move: Hi => /orP[Hi | ->]; last by rewrite orbT. by apply/orP; left; exact: (leq_trans (ltnW Hd) Hi). congr (_ * _); rewrite subSn //; apply IHi. - case: d H0d Hd => d //= _ _. by rewrite subSS; apply leq_subr. - move: Hi => /orP[Hi | ->]; last by rewrite orbT. apply/orP; left; apply: (leq_trans _ Hi). by rewrite ltnS; apply leq_subr. 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