proposition: Lemma limit_CE2: limit_v2 omega_plus_n (cons one 1 zero).
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 => ->; rewrite T1ltn0 if_same if_simpl; case n => // /and3P [_ nb ltb] _. move:nb ltb; case b => //; first by move => _ _; exists 0. move => a' n' b' /and3P [_ _ ltb] /=. rewrite T1lt1 T1ltn0 !if_same if_simpl => /eqP az. move: ltb; rewrite az /phi0 T1lt1 => /eqP ->. by exists n'; rewrite T1le_consE T1ltnn ltnn ! eqxx T1lenn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)