proposition: Lemma leq_Greene k (u1 : seq T1) (u2 : seq T2) : ksupp_inj k u1 u2 -> Greene_rel R1 u1 k <= Greene_rel R2 u2 k.
proof: Proof. Proof using. move=> Hinj; rewrite /= /Greene_rel /Greene_rel_t. set P1 := ksupp R1 (in_tuple u1) k. have : #|P1| > 0. rewrite -cardsE card_gt0; apply/set0Pn. by exists set0; rewrite in_set; apply: ksupp0. move/(eq_bigmax_cond (fun x => #|cover x|)) => [ks1 Hks1 ->]. move/(_ _ Hks1): Hinj => [] [ks2 /andP[/eqP ->] Hks2]. exact: (leq_bigmax_cond (F := fun x => #|cover x|)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype