proposition: Lemma next_fix_point_small f C (E:= cnext C): infinite_c C -> normal_ofs f -> (forall x, inc x E -> inc (f x) E) -> (forall x, inc x E -> inc (the_least_fixedpoint_ge f x) E).
proof: Proof. move => icE nf fee x xE. have [pa pb pc] := (cnext_pr1 (proj1 icE)). have [qa qb qc qd]:= (induction_defined_pr f x). move: (image_smaller (proj1 qb));rewrite qa (surjective_pr0 qb)=> sa. apply: cnext_sup => //. by apply: (cleT sa); rewrite cardinal_Nat; apply /infinite_c_P2. move => t /(proj2 qb); rewrite qa; move => [z zN ->]; move: z zN. apply: Nat_induction; [by ue | by move => n nN /fee hr; rewrite qd]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)