proposition: Lemma limit_prop x: T1nf x -> T1limit x -> limit_of (limit_fct x) x.
proof: Proof. elim:x => // a Ha n b Hb np /=. move/and3P: np => [sa sb sc]. have nc: forall m, T1nf (cons a m zero) by move => m; rewrite /= andbT. have Hc: forall m, (cons a m.+1 zero) = (cons a m zero) + phi0 a. by move => m; rewrite /phi0 /= T1ltnn addn0. case pa: (a==zero) => //; case bz: (b==zero); last first. by move /(Hb sb) => sd; rewrite -(add_to_cons n sc); apply: limit1. rewrite (eqP bz) => _. case isa: (T1is_succ a). have aux: (limit_of (phi3 (T1pred a)) (phi0 a)). by rewrite {2} (succ_pred sa isa); apply: limit3; apply: nf_pred. by case n => //= m; rewrite Hc; apply:limit1. move: (limit_pr1 a); rewrite pa isa /= addbF => la. have aux: (limit_of (phi2 (limit_fct a)) (phi0 a)) by apply: limit2; apply: Ha. by case n => //= m; rewrite Hc; apply:limit1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)