proposition: Lemma limit3 a: T1nf a -> limit_of (phi3 a) (phi0 (T1succ a)).
proof: Proof. move => na. rewrite /limit_of nf_phi0 nf_succ //; split => //. by move => n l nm /=; rewrite nm eqxx T1ltnn. split; first by move => n; rewrite /= succ_lt. case => //; first by exists 0; rewrite T1le0n. move => a' n b /and3P [na' _ _] /=. rewrite T1ltn0 !if_same if_simpl lt_succ_le_3 // T1le_eqVlt => aa. by exists n.+1; move: aa; rewrite T1le_consE ltnSn; case (T1ltgtP a a'). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)