proposition: Lemma tarski1 r f: complete_lattice r -> increasing_fun f r r -> complete_lattice (induced_order r (fixpoints f)).
proof: Proof. move => [or clr][_ _ [ff sf tf] incf]. set fif := fixpoints f. have fs: sub fif (substrate r) by rewrite/fif/fixpoints sf; apply: Zo_S. move: (iorder_osr or fs) => [oa sra]. apply Exercise1_11b => //; rewrite iorder_sr //. move => X xf; move: (sub_trans xf fs) => xsr. move: (supremum_pr1 or (proj1 (clr _ xsr))). set w := (supremum r X); move /(lubP or xsr) => [[pa pb] pc]. have ta: inc w (source f) by rewrite sf. have ra: gle r w (Vf f w). apply: pc; split; first by rewrite - tf; Wtac. by move => y yx; move: (xf _ yx) => /Zo_P [_ <-]; apply: incf; apply: pb. set B := Zo (substrate r) (fun t => gle r w t /\ gle r (Vf f t) t). have bsr: sub B (substrate r) by apply: Zo_S. move: (infimum_pr1 or (proj2 (clr _ bsr))). set z := (infimum r B); move /(glbP or bsr) => [[qa qb] qc]. have rb: lower_bound r B (Vf f z). split; first by rewrite - tf; Wtac. move => y yb; move: (qb _ yb) => yz; move: (incf _ _ yz) => sa. move: yb => /Zo_hi [_] sb; order_tac. move: (qc _ rb) => rc; move: (incf _ _ rc) => rd. have re: gle r w (Vf f z). have h: lower_bound r B w by split; [ order_tac | move => y /Zo_hi []]. by move: (incf _ _ (qc _ h)) => h1; order_tac. have rf: inc (Vf f z) B by apply: Zo_i; [ order_tac | split => //]. move: (qb _ rf) => rg. have rh: Vf f z = z by order_tac. have ri: inc z fif by apply: Zo_i => //; rewrite sf;order_tac. have pd: (substrate (induced_order r fif)) = fif by rewrite iorder_sr. have pe: sub X (substrate (induced_order r fif)) by ue. exists z; apply /(lubP oa pe); split. split; first by rewrite pd. move => y yx; apply /iorder_gle0P => //; first by apply: xf. move: (pb _ yx) => yw; rewrite -rh; order_tac. move => t []; rewrite pd => sa sb; apply /iorder_gle0P => //. move: (fs _ sa) => sc. apply: qb; apply: Zo_i => //; split. apply: pc;split;[by apply: fs | move => s sy; exact: (iorder_gle1 (sb _ sy))]. by move /Zo_P: sa => [_ ->]; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)