proposition: Lemma normal_fix_points_similar f C (E:= cnext C) (Xi := Zo E (fun z => f z = z)): infinite_c C -> normal_ofs f -> (forall x, inc x E -> inc (f x) E) -> (ord_cofinal Xi E) /\ cardinal Xi = E.
proof: Proof. move => icE nf fee. suff ha: ord_cofinal Xi E by split => //;apply:ord_cofinal_p4. split => //; first by apply: Zo_S. move => x xE. move: (next_fix_point_small icE nf fee xE). move/(cnextP (proj1 icE)): (xE) => [ox ob]. move: (normal_ofs_fix nf ox) => []; set y := the_least_fixedpoint_ge f x. by move => qa qb _ qc; exists y => //; apply:Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)