proposition: Lemma Exercise2_7B2 F: cofinal r F -> worder (induced_order r F) -> exists2 u, inc u closures & (fixpoints u) = F.
proof: Proof. move => [pa pb] pc. pose M x:= Zo F (gle r x). pose u x := the_least (induced_order r (M x)). have Ha x: inc x E -> nonempty (M x). by move/pb =>[y yF le]; exists y; apply/Zo_P. have Hb x: inc x E -> sub (M x) (substrate (induced_order r F)). by move => xE; rewrite iorder_sr//; apply: Zo_S. have Hc x: inc x E -> [/\ inc (u x) F, gle r x (u x)& forall t, inc t F -> gle r x t -> gle r (u x) t]. move => xE; move: (Hb _ xE) => hb. have hc: sub (M x) F by apply/Zo_S. have hd:= (sub_trans hc pa). move: (iorder_osr or hd) => [qa qb]. move: (proj2 pc _ hb (Ha _ xE)) => [y]; rewrite iorder_trans // => yl. move:(the_least_pr2 qa yl); rewrite -/(u x) => ->. case: yl; rewrite iorder_sr //;move/Zo_P => [he hf] hg; split => // t tf tg. have: inc t (M x) by apply/Zo_P. by move/hg/iorder_gle1. have Hd x: inc x F -> u x = x. move => xF; move: (Hc _ (pa _ xF))=> [ha hb hc]. have lexx: gle r x x by move: (pa _ xF) => xsr; order_tac. move: (hc _ xF lexx)=> leux; order_tac. have ax: lf_axiom u E E by move => x /Hc/proj31/pa. have He: function_prop (Lf u E E) (substrate r) (substrate r). by saw; apply: lf_function. exists (Lf u E E). apply/Zo_P; split; first by apply/functionsP. split. - split => // a b lab. move: (arg1_sr lab) (arg2_sr lab) => aE bE. rewrite ! LfV//;move: (Hc b bE)=> [qa qb _]; apply: (proj33 (Hc a aE) _ qa); order_tac. - move => x xE; rewrite LfV//; exact: (proj32 (Hc _ xE)). - move => x xE; move: (proj31 (Hc _ xE))=> uF. by rewrite (LfV ax xE) (LfV ax (pa _ uF)); apply: Hd. set_extens t. move /Zo_P; aw; move => [tE]; rewrite LfV // => <-. exact:(proj31 (Hc _ tE)). move => tF; move: (pa _ tF) => tR; apply/Zo_i; aw; trivial. by rewrite LfV//; apply: Hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)