proposition: Lemma limit3 x: limit_of (phi3 [zero,zero,x]) [zero, zero, T3succ x].
proof: Proof. split. by move => n m; rewrite !phi3v T3lt_consE T3ltnn eqxx => ->. by move => n; rewrite phi3v T3lt_consE lt_omega1 eqxx /= succ_lt. case => //; first by move => _ h; exists 0. move => a b c n d /and5P[_ _ nc _ _]; rewrite -/T3nf in nc. rewrite psi_lt1 T3lt_psi' !T3ltn0 !T3lt0n !andbF /= => h. exists (n.+1); rewrite phi3v T3le_consE ltnS leqnn if_simpl -/(orb _ _). move: h; rewrite lt_succ_le_3 //;case/orP. move => /and3P [sa sb sc]; rewrite (eqP sa) (eqP sb). by move: sc; rewrite T3lt_psi /lt_psi eqxx T3ltnn /T3le /=;case:(T3ltgtP x c). case xz: (x==zero). rewrite (eqP xz) /= /T3le -/one; case (T3ltgtP [a, b, c] one) => //. by rewrite !andbF. case ha: ([a,b,c] == one) => hh. by rewrite (eqP ha) T3lt_consE T3lt_psi /lt_psi eqxx T3lt0n xz. rewrite orbC; apply: (T3le_trans _ (T3ltW (T3lt_psi_c zero zero x))). by move: hh; rewrite (succ_psi_lt2 _ (negbT ha)) andbA; case /orP => /andP []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)