proposition: Lemma T2lt_psi_b a b: b < [a,b].
proof: Proof. elim: b a => // a _ b Hb n c _ x. have ha:= (T2le_psi1 a b n c). have hb:= (T2lt_le_trans (Hb a) ha). rewrite T2lt_consE /lt_psi; case: (T2ltgtP a x). + rewrite /= !orbF if_simpl => ax. by apply: (T2lt_trans (Hb x)); rewrite T2lt_consE /lt_psi hb eqxx !orbT. + by move => _ /=; rewrite orbC -/(T2le _ _) ha. + by move => _ /=; rewrite hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)