proposition: Lemma plactic_filter_gt L u v : u =Pl v -> [seq x <- u | (L > x)%O] =Pl [seq x <- v | (L > x)%O].
proof: Proof. Proof using. move=> H; case Hfu : [seq x <- u | (L > x)%O] => [| fu0 fu']. suff -> : [seq x <- v | (L > x)%O] = [::] by apply plact_refl. apply/eqP; move: Hfu => /eqP; apply contraLR. rewrite -!has_filter => /hasP[x Hx HgtnX]. apply/hasP; exists x; last exact HgtnX. by move: H => /plact_homog/perm_mem ->. have := maxLP fu0 fu' => /allP; rewrite -Hfu => HML. set ML := maxL fu0 fu'. have Heq: {in u, >%O L =1 >=%O ML}. move=> x Hx /=. apply/idP/idP => Hxl. - by apply: HML; rewrite mem_filter Hx /= Hxl. - have:= in_maxL fu0 fu'; rewrite -Hfu; rewrite mem_filter /= => /andP[HMLL _]. exact: le_lt_trans Hxl HMLL. rewrite (eq_in_filter Heq). have {}Heq: {in v, >%O L =1 >=%O ML}. by move=> x /=; move: H => /plact_homog/perm_mem <-; exact: Heq. rewrite (eq_in_filter Heq). exact: plactic_filter_ge. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr