proposition: Lemma normal_fix_cofinal C (E := cnext C) f: infinite_c C -> normal_function f E E -> ord_cofinal (fixpoints f) E.
proof: Proof. move => icE nf. have [[ff sf tf] _ _] := nf. split; first by rewrite - sf; apply: Zo_S. move => x xE. move: (next_fix_point_small1 icE nf xE); rewrite -/E - sf. set y := the_least_fixedpoint_ge (Vf f) x; move => [pa pb pc pd]. by exists y => //; apply/Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)