proposition: Lemma Greene_rel_cat k v w : Greene_rel (v ++ w) k <= Greene_rel v k + Greene_rel w k.
proof: Proof. Proof using HR. rewrite /disjoint /=. rewrite (_ : Greene_rel_t _ _ _ = Greene_rel_t R [tuple of (in_tuple v) ++ (in_tuple w)] k); first by apply: Greene_rel_t_cat. have Hsz : size (v ++ w) = (size v + size w) by rewrite size_cat. rewrite -(Greene_rel_t_cast _ Hsz); congr (Greene_rel_t R _ k). apply: eq_from_tnth => i; rewrite tcastE. case: (altP (size v + size w =P 0)) => Hsize. by exfalso; move: i; rewrite Hsize => [][]. have x0 : Alph by rewrite -Hsz in i Hsize; case: (v ++ w) Hsize. by rewrite !(tnth_nth x0). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype