proposition: Lemma limit_CE3: limit_v2 omega_plus_n (cons one 0 T1omega).
proof: Proof. by move: limit_CE1 => [sa sb]; split => // y _; apply: sb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)