proposition: Lemma Greene_rel_t_0 : Greene_rel_t 0 = 0.
proof: Proof. Proof using. rewrite /Greene_rel_t /=. apply/eqP; rewrite eqn_leq; apply/andP; split; last by []. apply/bigmax_leqP => S. rewrite /ksupp => /and3P[HS _ _]. have -> : S = set0 by apply/eqP; rewrite -cards_eq0 eqn_leq HS. by rewrite /cover big_set0 cards0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype