proposition: Lemma limit_CE1: limit_v1 omega_plus_n (cons one 0 T1omega).
proof: Proof. split; first by move => n. move => y ;case: y => //; first by exists 0; rewrite T1le0n. move => a n b /=; case: (T1ltgtP a one) => //. by rewrite T1lt1 => /eqP -> _; exists 0. move => ->; case: eqP => // ->; case: b => //; first by exists 0. move => a' n' b' /=; rewrite /phi0 T1lt1 T1ltn0 !if_same if_simpl. move /eqP ->; exists (n'.+1); rewrite T1le_consE T1ltnn !eqxx ltnn. by rewrite T1le_consE T1ltnn !eqxx ltnSn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)