proposition: Lemma normal_ofs_fix x f: normal_ofs f -> ordinalp x -> least_fixedpoint_ge f x (the_least_fixedpoint_ge f x).
proof: Proof. move => nf ox. move/normal_ofs_equiv1:(nf)=> nf1; apply: (normal_ofs_fix1 nf1 (ole0x ox)). exact:(osi_gex (proj1 nf) ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)