proposition: Lemma limit_pr x y: T2limit x -> y < x -> T2succ y < x.
proof: Proof. elim: x y; [ by [] |move => a _ b _ n c Hc y /=]. case: y. rewrite T2gt1 andTb !T2eqE !andbT !andbA. by case sa: ((a == zero) && (b == zero)). move => a' b' n' c';rewrite /T2succ -/T2succ => hh. case pa: ([a', b'] == one). rewrite T2lt_consE /= T2lt_consE -!T2lt_psi (eqP pa). have ->: ((zero == a) && (zero == b)) = (one == [a,b]). by rewrite T2eqE !eqxx !andbT. move: hh; rewrite (eq_sym _ one); case: (T2ltgtP one [a,b]) => //. by rewrite T2lt1. rewrite T2lt_consE T2lt_consE. case ha:(lt_psi a' b' a b) => //; case hb: ((a' == a) && (b' == b)) => //. case: (ltngtP n' n) => // _ hc;apply: Hc => //. move: hh hc; move/andP:hb => [/eqP <- /eqP <-]; rewrite pa. by case /orP => //; move /eqP ->; rewrite T2ltn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)