proposition: Lemma cnvar_symh i : (i <= m) || (n <= m) -> cnvarsym 'h_i = 'h_i.
proof: Proof. move=> Hi; rewrite !symh_to_syme. rewrite linear_sum /=; apply eq_bigr => la _. rewrite linearZ rmorph_prod /=; congr(_ *: _). apply eq_big_seq => j /intpartn_leq le_ji; apply cnvar_syme. move: Hi => /orP[Hi | ->]; last by rewrite orbT. by apply/orP; left; apply: (leq_trans le_ji Hi). 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