proposition: Lemma non_cont_ex2: ~ ocontinuous_at (fun t => t +o t) omega0.
proof: Proof. move: OS_omega => oo hyp. move:(osum_Meqlt olt_0omega oo); rewrite (osum0r oo) => ll. move:(proj2 hyp _ ll) => [y ys yp]. by case:(olt_ltT (yp y (oleR (proj31_1 ys)) ys) (osum2_lt_omega ys ys)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)