proposition: Lemma Greene_rel_t_cat k : Greene_rel_t R [tuple of V ++ W] k <= Greene_rel_t R V k + Greene_rel_t R W k.
proof: Proof. Proof using HR. rewrite /Greene_rel_t; set tc := [tuple of V ++ W]. have H : 0 < #|k.-supp[R, tc]| by apply/card_gt0P; exists set0; apply: ksupp0. case: (@eq_bigmax_cond _ (mem k.-supp[R, tc]) scover H) => ks Hks ->. pose PV := lsplit @: ks; pose PW := rsplit @: ks. move: Hks => /and3P[Hcard Htriv /forallP Hcol]. have HV : PV \is a k.-supp[R, V]. rewrite /ksupp; apply/and3P. split; first exact: (leq_trans (leq_imset_card _ _) Hcard). - exact: preimset_trivIset. - apply/forallP=> stmp; apply/implyP => /imsetP[s Hs -> {stmp}]. by rewrite extlsplit; apply: sorted_extract_cond; move/(_ s): Hcol; rewrite Hs. have HleqV := (@leq_bigmax_cond _ _ scover _ HV). have HW : PW \is a k.-supp[R, W]. rewrite /ksupp; apply/and3P. split; first exact: (leq_trans (leq_imset_card _ _) Hcard). - exact: preimset_trivIset. - apply/forallP=> stmp; apply/implyP => /imsetP[s Hs -> {stmp}]. by rewrite extrsplit; apply: sorted_extract_cond; move/(_ s): Hcol; rewrite Hs. have HleqW := (@leq_bigmax_cond _ _ scover _ HW). have -> : scover ks = scover PV + scover PW. rewrite /= cutcover. have:= disjoint_inj (cover PV) (cover PW). rewrite -((leq_card_setU _ _).2) => /eqP ->. by rewrite (card_imset _ (@lshift_inj _ _)) (card_imset _ (@rshift_inj _ _)). exact: leq_add. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype