proposition: Lemma shape_instabnrowinv1 t nrow yam : is_yam (nrow :: yam) -> shape t == evalseq (nrow :: yam) -> shape (invinstabnrow t nrow).1 == evalseq yam.
proof: Proof. Proof using. elim: nrow yam t => [|nrow IHnrow] yam t Hyam. - case: t => [/= | r0 t]; first by case (evalseq yam). rewrite evalseq_cons => Hshape. move/is_yam_tl : Hyam => /is_part_eval_yam Hpart. case: r0 Hpart Hshape => [/= | l0 [| l1 r0'] ] Hpart Hshape /=. * by case: (evalseq yam) Hshape. * case: (evalseq yam) Hpart Hshape => //=. case => [ | //] l /andP[]; rewrite leqn0. by move/part_head0F => ->. * move: Hshape; rewrite size_belast /=. by case (evalseq yam). - case: t => [/= | r0 t]; first by case (evalseq yam). rewrite evalseq_cons => /eqP Hshape. have Hsz0 : (size r0) = head 0 (evalseq yam). by move: Hshape => /=; case (evalseq yam) => [|s0 s] [] ->. move/(congr1 behead): Hshape. rewrite behead_incr_nth -evalseq_decr_yam /= => /eqP{}/IHnrow Hrec. have Hnnilyam := yam_tail_non_nil Hyam. move: Hyam => /is_yam_decr; rewrite [decr_yam _]/= => {}/Hrec /=. case Hinv: (invinstabnrow t nrow) => [tin l] /=. have:= size_invins l r0; rewrite /invins. case Hbump: (invbumprow l r0) => [t0r l0r] /= -> /eqP ->. rewrite {Hbump t0r l0r Hinv tin l} evalseq_decr_yam Hsz0 {Hsz0 r0}. case: yam Hnnilyam => [// | a b _]. have: evalseq (a :: b) != [::] by case: a => [| a] /=; case (evalseq b). by case (evalseq (a :: b)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab