proposition: Lemma olimit_econst f x l: ordinalp l -> econst f x l -> olimit f x l.
proof: Proof. move => ol [y lyx fv]. split; first by exists y => // i la lb;rewrite (fv i la lb); apply: oleR. by move => m lm; exists y => // i la lb; rewrite (fv i la lb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)