proposition: Lemma RabcLeqX a b c : (a < b <= c)%O -> hypRabc <=%O a b c.
proof: Proof. move=> H; constructor. - move=> x y z; exact: le_trans. - by move: H => /andP /= []. - by move: H => /andP /= []; rewrite ltNge. - by move: H => /andP /= [H1 _] /= x H2; exact: (le_trans H2 (ltW H1)). - by move: H => /andP /= [H1 _] /= x H2; exact: (le_trans (ltW H1) H2). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene