proposition: Lemma succ_psi_lt x a b : [a, b] != one -> x < [a,b] -> T2succ x < [a,b].
proof: Proof. move => yn1; case: x => //; first by rewrite /= T2gt1 yn1. move => a' b' n d /=. case: ([a', b'] == one);rewrite !T2lt_consE ltn0 T2ltn0 !if_same if_simpl. move: yn1; rewrite - !T2lt_psi -/one eq_sym; case: (T2ltgtP one [a,b]) => //. by rewrite T2lt1. by move => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)