proposition: Lemma limit_pr x y: T3limit x -> y < x -> T3succ y < x.
proof: Proof. elim: x y; [ by [] |move => a _ b _ c _ n d Hd y /=]. case: y. rewrite /T3succ T3gt1 andTb T3eqE => H1 _. apply /negP => /and5P [sa sb sc _ _]; move: H1; rewrite /all_zero sa sb sc//. move => a' b' c' n' d';rewrite /T3succ -/T3succ !all_zeroE => hh. case pa:([a', b', c'] == one); rewrite T3lt_consE => h; rewrite T3lt_consE. move: h hh; rewrite (eqP pa). by case: (T3ltgtP one [a, b, c]) => // ->; rewrite eqxx. move: h;case:(T3ltgtP [a',b',c'] [a, b, c]) => // _. move: hh; case: eqP => // _ hh;case: (ltngtP n' n) => //; case /orP: hh => hh. by rewrite (eqP hh) T3ltn0. by move => _; apply: Hd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)