proposition: Lemma lt_succ_le_2 a b: T1nf a -> a < T1succ b -> a <= b.
proof: Proof. elim: a b; first by move => b;rewrite T1le0n. move => a' _ n' b' Hb; case; first by rewrite /= ! T1ltn0 ! if_same. case. case a' => // n b; move /T1nf_finite ->. rewrite /= if_same if_simpl ltnS T1le_consE T1le0n T1ltnn eqxx leq_eqVlt. case: (ltngtP n' n) => //. move => a'' n'' b'' n b /T1nf_consb H; rewrite T1le_consE /=. case: (T1ltgtP a' (cons a'' n'' b'')) => //. by case: (ltngtP n' n) => //= _ _; apply: Hb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)