proposition: Lemma omegasf_symh i : i <= n -> omegasf 'h_i = 'e_i.
proof: Proof. have [k/ltnW] := ubnP i; elim: k => [| k IHk] in i *. by rewrite leqn0 => /eqP ->; rewrite symh0 syme0 rmorph1. rewrite leq_eqVlt => /orP[/eqP->{i} lt_kn |]; last by rewrite ltnS => /IHk. rewrite symh_symeE // rmorph_sum //= syme_symhE //. rewrite !big_nat; apply eq_bigr => [][|j]//; rewrite !ltnS leq0n /= => le_jk. rewrite subSS rmorphM /= linearZ /= IHk ?leq_subr //; first last. by apply ltnW; apply: (leq_ltn_trans (leq_subr _ _) lt_kn). by rewrite omegasf_syme // (leq_ltn_trans le_jk lt_kn). 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