proposition: Lemma T2le_cons_le a b n c a' b' n' c': (cons a b n c <= cons a' b' n' c') -> [a,b] <= [a',b'].
proof: Proof. rewrite T2le_consE - T2lt_psi. case h: ([a, b] < [a', b']); first by move => _; exact :(T2ltW h). case h1: ((a == a') && (b == b')) => // _. by move/andP:h1 => [/eqP -> /eqP ->]; apply: T2lenn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)