proposition: Lemma const_continuous v: ordinalp v -> ocontinuous (fun i => v).
proof: Proof. move => ov x xl; move: (limit_pos xl) => xp; move: (proj31 xl) => ox. by apply: olimit_econst => //; exists \0o. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)