proposition: Lemma normal_continuous f: normal_ofs f -> ocontinuous f.
proof: Proof. move =>[ha hb]x xl; rewrite /ocontinuous_at (hb x xl). by apply:(olim_sup xl) => i j la lb; apply: sincr_incr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)