proposition: Lemma succ_psi_lt2 a b x: [a, b] != one -> ([a, b] <= T2succ x) = ([a, b] <= x).
proof: Proof. move => ha;symmetry. case (T2leP [a, b] (T2succ x)). by rewrite !T2leNgt; apply: contra; apply:succ_psi_lt. by move => hb; move: (T2lt_trans (succ_lt x) hb);rewrite T2ltNge; move /negbTE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)