proposition: Lemma iclosed_normal_ofs1 f u: ordinalp u -> normal_ofs1 f u -> iclosed_proper (fun z => exists2 x, u <=o x & z = f x).
proof: Proof. move => ou [na nb]. have ha:= (ofs_sincru na). have [_ [b ub h]] := (osum_increasing5 ou na). split; last first. apply:unbounded_non_coll => x ox. case: (oleT_ee (proj32 ub) ox) => bx. exists (f x); [ by apply:h | exists x => //;apply: oleT ub bx]. exists (f b); [exact: (oleT bx (h _ (oleR (proj32 ub)))) |by exists b]. split; first by move => x [y /ha uy ->]. move => F Fi nef. pose p z t:= u <=o t /\ z = f t. have pm z t: p z t -> t <=o (omax b z). move => [pa ->]; move:(ha _ pa) => oz. move: (omax_p1 (proj32 ub) oz) => [ma mb]. case:(oleT_ee (proj32 ub) (proj32 pa)) => bt. exact:(oleT (h _ bt) mb). exact: (oleT bt ma). pose g z := least_ordinal (p z) (omax b z). have Cp a: u <=o a -> u <=o (g (f a)) /\ (f a) = f (g (f a)). move => az; rewrite /g/least_ordinal; set E := Zo _ _ . have osE:ordinal_set E by move => t/Zo_P [_] [/proj32]. have pp: p (f a) a by []. move: (pm _ _ pp) => le1. have neE: nonempty E by exists a; apply:Zo_i =>//; apply/(oleP (proj32 le1)). by move:(least_ordinal0 osE neE) => [_ /Zo_P [ _ qb] _]. have CP1 a: u <=o a -> a = g (f a). move => au; move: (Cp _ au) => [pa pb]. case: (oleT_ell (proj32 au) (proj32 pa)) => // hb. by move: (proj2 (na _ _ au hb)); rewrite {1} pb. by move: (proj2 (na _ _ pa hb)); rewrite - pb. have CP2 x: inc x F -> p x (g x) by move /Fi => [t /Cp [ta tb] ->]. set E:= fun_image F g. have Fv: F = fun_image E f. set_extens w. by move => wF; rewrite(proj2 (CP2 _ wF)); apply: funI_i; apply: funI_i. by move /funI_P => [x /funI_P [z zf ->] ->]; rewrite - (proj2 (CP2 _ zf)). have pa: forall x, inc x E -> u <=o x /\ g (f x) = x. by move => w /funI_P [z /CP2 [wa wb] ->]; rewrite - wb. have Ea: (forall x, inc x E -> u <=o x) by move => x /pa []. have [t0 t0f] := nef. have fit0: inc (g t0) E by apply/funI_P; ex_tac. have ne: nonempty E by ex_tac. have: u <=o \osup E. by apply: (oleT (Ea _ fit0)); apply: ord_sup_ub => // t /Ea []. by move: (nb _ Ea ne); rewrite -Fv => ->; exists (union E). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)