proposition: Lemma Exercise1_13b r G (ir := fun x => induced_order r (upper_bounds G r x)) (g := Lf (fun x => the_least (ir x)) (substrate r) (substrate r)): order r -> sub G (substrate r) -> (forall x, inc x (substrate r) -> has_least (ir x)) -> (closure g r /\ (G = fixpoints g)).
proof: Proof. move => or Gsr gu. set (E:= substrate r). have Ha:forall x, inc x E -> sub (upper_bounds G r x) E. move=> x xE; apply: sub_trans Gsr=> //; apply: Zo_S. pose h x := the_least (ir x). have pg: forall x, inc x E -> least (ir x) (h x). move=> x xst; apply: the_least_pr; last by apply: gu. by apply: (proj1 (iorder_osr or _)); apply: Ha. have Hc:forall x y, inc x E -> inc y G -> gle r x y -> gle r (h x) y. move=> x y xE yG xy; move: (pg _ xE)=> []. rewrite/ir iorder_sr//;last by apply: Ha. have ys: inc y (upper_bounds G r x) by apply: Zo_i. by move=> aa bb; move: (iorder_gle1 (bb _ ys)). have Hd:forall x, inc x E -> [/\ inc (h x) E, inc (h x) G & gle r x (h x)]. move=> x xE; move: (pg _ xE)=> [p1 p2]. move: (Ha _ xE) => s1; move: p1; rewrite/ir. rewrite iorder_sr//; move /Zo_P=> [q1 q2];split;fprops. have He:forall x, inc x G -> (h x) = x. move=> x xG; move: (Gsr _ xG) => xE. have xs: gle r x x by order_tac. move: (proj33 (Hd _ xE)) (Hc _ _ xE xG xs) => le2 le1; order_tac. have ta: lf_axiom h E E by move=> t tE; case: (Hd _ tE). have gv: (forall x, inc x E -> Vf (Lf h E E) x = h x) by move => x xE; rewrite LfV//. have fp:function_prop (Lf h E E) (substrate r) (substrate r). by saw; apply: lf_function. split. split. split => //; aw=> x y xy. have xE: inc x E by rewrite /E; order_tac. have yE: inc y E by rewrite /E; order_tac. rewrite (gv _ xE)(gv _ yE); move: (Hd _ yE) => [p1 p2 p3]. apply: Hc => //; order_tac. by move=> x xE; rewrite (gv _ xE); case: (Hd _ xE). move=> x xE; move: (Hd _ xE) => [p1 p2 p3]. by rewrite (gv _ xE) (gv _ p1); apply: He. rewrite /g;set_extens t. move => tG; move: (Gsr _ tG)=> tE; apply : Zo_i => //; aw; trivial. by rewrite LfV//; apply: He. move => /Zo_P []; rewrite lf_source => te; rewrite LfV// => <-. by move: (Hd _ te) => [_ ok _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)