proposition: Lemma normal_ofs_limit f x: normal_ofs f -> limit_ordinal x -> limit_ordinal (f x).
proof: Proof. move => /(normal_ofs_equiv2 OS0) nf lx; apply:(normal_ofs_limit1 nf _ lx). by apply: limit_pos. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)