proposition: Lemma choose_one_countE shr innev shape mini maxi row l : is_part innev -> is_skew_yam innev shr row -> is_skew_yam innev shape (l :: row) -> included shape outev -> mini <= l <= maxi -> is_row (l :: row) -> (count_mem l) (one_letter_choices shr mini maxi) = 1.
proof: Proof. Proof using . rewrite /one_letter_choices count_filter => Hpart Hrow Hlrw Hincl /andP[Hmin Hmax] Hisrow. move/(_ _ (hyper_yam_of_eval Hpart)): Hrow => /= /andP[Hyamrow /eqP Hshr]. move/(_ _ (hyper_yam_of_eval Hpart)): Hlrw => /= /andP[Hyamlrow /eqP Hshape]. rewrite (eq_count (a2 := pred1 l)); first last. move=> i /=; case (i =P l) => [Hi | //]; subst i. have -> /= : is_add_corner shr l by rewrite -Hshr; exact: is_add_corner_yam. move: Hincl => /includedP[_ Hincl]. apply: (leq_trans _ (Hincl l)). rewrite -Hshape /= Hshr. by rewrite nth_incr_nth eq_refl add1n ltnS. rewrite (count_uniq_mem _ (iota_uniq _ _)) mem_iota Hmin /=. set m := minn _ _. suff : l <= m. case (ltnP mini m.+1) => [/ltnW | ] H Hl. - by rewrite (subnKC H) ltnS Hl. - have:= H; rewrite {1}/leq => /eqP ->. by rewrite addn0 (leq_ltn_trans Hl H). rewrite {}/m leq_min Hmax andbT. apply is_part_incr_nth_size; rewrite -Hshr. - exact: (is_part_eval_yam Hyamrow). - exact: (is_part_eval_yam Hyamlrow). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools combclass partition Yamanouchi ordtype tableau skewtab Schur_mpoly freeSchur therule