proposition: Lemma lt_succ_le_4 a b: T1nf b -> (a < b) = (T1succ a <= b).
proof: Proof. move => nb. case: (T1ltP a b). rewrite T1leNgt T1ltNge; case h: (b < T1succ a) => //. by rewrite(lt_succ_le_2 nb h). by move /le_succ_succ => /(T1lt_le_trans (succ_lt b)); rewrite T1leNgt => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)