proposition: Lemma lt_succ_le_3 a b: T2nf a -> (a < T2succ b) = (a <= b).
proof: Proof. move => na; case h:(a < T2succ b). by rewrite (lt_succ_le_2 na h). rewrite - h; case (T2ltP b a) => // ab; exact: (T2le_lt_trans ab (succ_lt b)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)