proposition: Lemma olimit_zero f x: olimit f x \0o <-> econst f x \0o.
proof: Proof. split; last by apply: olimit_econst; apply: OS0. move => [[y yl yp] hb]; exists y => // i i1 i2; move: (yp i i1 i2). by move/ole0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)