proposition: Lemma congr_row_2 a r l : is_row (a :: r) -> (l < a)%O -> a :: rcons r l =Pl a :: l :: r.
proof: Proof. Proof using. elim/last_ind: r => [_ _ //= | r rn]; first exact: plact_refl. case/lastP: r => [_ /=| r rn1]. - move/andP => [] Harn _ Hla; apply: rule_gencongr => //=. by rewrite Harn Hla !mem_cat !mem_seq1 eq_refl /= !orbT. - move=> IH; rewrite -rcons_cons => Hrow Hla. move/(_ (is_row_rconsK Hrow) Hla): IH => IH. apply (@plact_trans _ _ (a :: rcons (rcons (rcons r rn1) l) rn)) => //. + apply: plact_cons; rewrite !rcons_rcons -!cats1 -!catA. apply: plact_catr => /=; apply: rule_gencongr. have:= head_leq_last_row (is_row_rconsK Hrow); rewrite last_rcons => Harn1. have:= is_row_last Hrow. rewrite -rcons_cons last_rcons => Hrn1rn. by rewrite /= Hrn1rn (lt_le_trans Hla Harn1) !mem_cat !mem_seq1 eq_refl /= !orbT. + move: IH; rewrite -!rcons_cons; exact: plact_rcons. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr