proposition: Lemma limit_pr x y: T1limit x -> y < x -> T1succ y < x.
proof: Proof. elim: x y; [ by [] |move => a _ n b Hb y /= H1]. case: y; [ by move => _; move: H1; case: a |move => a' n' b' /=]. have aux: b' < b -> T1succ b' < b. case: (a==zero) H1 => // /orP []; first by move => /eqP ->; rewrite T1ltn0. by apply: Hb. case a'; first by rewrite /T1succ; move => _;move: H1; case: a. move => a'' n'' b''; case: a H1; [ done | move => u v w _ ]. simpl; rewrite T1eqE;case: (a'' < u) => //; case: eqP => // _. case:(n'' < v)%N => //; case e2: (n'' == v) => //; case: (b'' < w) => //. by case: eqP => //= _; case: (n' <n)%N => //; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)