proposition: Lemma T2lt_psi_a a b: a < [a,b].
proof: Proof. elim: a b => //a Ha b Hb n c _ x. have ha:= (T2lt_le_trans (Ha b) (T2le_psi1 a b n c)). have hb:= (T2lt_le_trans (T2lt_psi_b a b)(T2le_psi1 a b n c)). have hc :[b,x] < [cons a b n c, x] by rewrite T2lt_consE /lt_psi hb T2lt_psi_b. by rewrite T2lt_consE /lt_psi ha (T2lt_trans (Hb x) hc). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)