proposition: Lemma lt_succ_le_4 a b: T2nf b -> (a < b) = (T2succ a <= b).
proof: Proof. move => nb. case: (T2ltP a b). rewrite T2leNgt T2ltNge;case h: (b < T2succ a) => //. by rewrite(lt_succ_le_2 nb h). by move /le_succ_succ => /(T2lt_le_trans (succ_lt b)); rewrite T2leNgt => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)