proposition: Lemma not_hasincr_part : size la <= n -> ~~ hasincr -> is_part_of_n (d + #|h|) (rem_trail0 (mpart la + mesym1 h)%MM).
proof: Proof. Proof using . move=> Hsz /hasPn H. rewrite /mpart Hsz. apply/andP; split. - rewrite sumn_rem_trail0. rewrite (@sumn_nth_le _ n); last by rewrite size_map size_enum_ord. rewrite big_mkord. under eq_bigr do rewrite -tnth_nth -mnm_tnth 2!mnmE. rewrite big_split /=; apply/eqP; congr (_ + _)%N. + by rewrite -{2}(sumn_intpartn la) (sumn_nth_le Hsz) big_mkord. + rewrite -mdeg_mesym1 /mdeg. rewrite -map_tnth_enum big_map big_enum; apply eq_bigr => i _. by rewrite mnm_tnth. - apply/is_part_rem_trail0/(sortedP 0) => i. rewrite size_map size_enum_ord => Hi1. have Hi : i < n by apply: (ltn_trans _ Hi1). have {}/H : i \in iota 0 n.-1. rewrite mem_iota add0n. by case: n Hi1 {Hsz H Hi} => [//= | n'] /=; rewrite ltnS. have H0 : 0 < n by apply: (leq_ltn_trans _ Hi1). rewrite /mpart Hsz !(nth_map (Ordinal H0) 0) ?size_enum_ord // !mnmE. rewrite !nth_enum_ord //. have [_ /(_ i) H1] := is_partP _ (intpartnP la). case: (_ i \in h) (_ i.+1 \in h) => [] [] /=; rewrite ?addn1 ?addn0 => H2. + by rewrite ltnS. + exact: (leq_trans H1). + by rewrite ltn_neqAle -eqSS eq_sym H2 H1. + exact: H1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn