proposition: Lemma non_cont_ex1 x: limit_ordinal x -> ~ ocontinuous_at osucc x.
proof: Proof. move => xl. move/(olimit_succ _ _ (proj31 xl)) =>[y lyx yp]. move:(lyx) => [[oy ox _]]; case. exact:(osucc_inj oy ox (yp y (oleR oy) lyx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)