proposition: Lemma congr_row_1 r b l : is_row (rcons r l) -> (l < b)%O -> rcons (rcons r b) l =Pl b :: rcons r l.
proof: Proof. Proof using. elim/last_ind: r l => [| r rn IHr] l Hrow Hl. by rewrite /=; exact: plact_refl. have:= is_row_last Hrow; rewrite last_rcons => Hrnl. apply (@plact_trans _ _ (rcons (rcons (rcons r b) rn) l)). - rewrite !rcons_rcons -!cats1 -!catA !cat1s. apply: plact_catr; apply: rule_gencongr => /=. by rewrite Hl Hrnl !mem_cat !mem_seq1 eq_refl. - rewrite -rcons_cons; apply: plact_rcons. apply: (IHr _ (is_row_rconsK Hrow)). exact: le_lt_trans Hrnl Hl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr