proposition: Lemma Greene_rel_rev (leT : rel Alph) u : Greene_rel leT u =1 Greene_rel (fun y x => leT x y) (rev u).
proof: Proof. Proof using. move=> k; apply anti_leq; apply/andP; split. - apply leq_Greene; first exact: ksupp_inj_rev. - rewrite [X in _ <= X](eq_Greene_rel (R2 := fun x y => leT x y)). + apply leq_Greene; rewrite -{2}(revK u); exact: ksupp_inj_rev. + by move=> i j. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype