proposition: Lemma Exercise1_15a20 X x: sub X (substrate r) -> greatest_lower_bound r X x -> greatest_lower_bound (completion_order r) (fun_image X lobs) (lobs x).
proof: Proof. move=> Xsr /(glbP or Xsr) [[xX xu] xlu]. set Y:= fun_image X lobs. have Yc: (sub Y (completion r)). move=> y /funI_P [z zX ->]; apply: Exercise1_15a8. by move=> t /set1_P ->; apply: Xsr. have oc: order (completion_order r) by rewrite /completion_order; fprops. have sr: substrate (completion_order r) = completion r. by rewrite /completion_order (proj2(sub_osr _)). case: (emptyset_dichot Y) => ye. have xE: (X = emptyset). apply /set0_P => u uX; case: (in_set0 (x:=lo_bounds r (singleton u))). rewrite -ye; apply /funI_P; ex_tac. have -> : lobs x = substrate r. apply: extensionality; first by apply: Zo_S. move=> t tsr; apply: Zo_i =>//; split => //;move=> y /set1_P ->; apply: xlu. by split => //; rewrite xE; move=> u /in_set0. rewrite ye glb_set0 //; exact: Exercise1_15a13. suff : lobs x = uplo_bounds r (intersection Y). move=> ->;apply: (Exercise1_15a15 Yc ye). have p1: (sub (lobs x) (intersection Y)). move=> u ut; apply: setI_i =>// y /funI_P [z zX slb]. move: ut => /Zo_P [usr [_ aux]]; move: (aux _ (set1_1 x)) => leux. rewrite slb; apply: Zo_i => //; split => //; move=> v /set1_P ->. move: (xu _ zX) => xz; order_tac. apply: extensionality. move: (Exercise1_15a5 (set1_sub xX)). by rewrite -/(lobs x);move => <-; apply: Exercise1_15a3. move=> u /Zo_P [usr [_ leu]]. apply: Zo_i => //; split =>//y /set1_P ->; apply: xlu; split => //. move=> v vX; move: (Xsr _ vX) => vs; apply: leu; apply: Zo_i => //;split => //. have aux: (inc (lo_bounds r (singleton v)) Y) by apply/funI_P;ex_tac. move=> w wi; move: (setI_hi wi aux) => /Zo_P [wsr[_ q]]. apply: (q _ (set1_1 v)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)