proposition: Lemma Exercise1_15a19 X x: sub X (substrate r) -> least_upper_bound r X x -> least_upper_bound (completion_order r) (fun_image X lobs) (lobs x).
proof: Proof. move=> Xsr /(lubP or Xsr) [[xX xu] xlu]. have Yc: (sub (fun_image X lobs) (completion r)). move=> y /funI_P [z zX ->]; apply: Exercise1_15a8. by move=> t /set1_P ->; apply: Xsr. suff : uplo_bounds r (union (fun_image X lobs)) = lobs x. move=> <-;apply: (Exercise1_15a14 Yc). apply: extensionality. move: (Exercise1_15a5 (set1_sub xX)); rewrite -/(lobs x). move => <-; apply: Exercise1_15a3. move=> u /setU_P [y uy /funI_P [z zX slb]]. move: uy; rewrite slb; move /Zo_P => [usr [_ ulb]]. move: (ulb _ (set1_1 z)) (xu _ zX) => le1 le2. apply: Zo_i=> //; split => //; move => v /set1_P ->; order_tac. move=> u => /Zo_P[usr [_ leu]]; move: (leu _ (set1_1 x)). move=> ux; apply: Zo_i => //; split => //. move=> y /Zo_P [ysr [_ yu]]. suff: (gle r x y) by move=> xy; order_tac. apply: xlu; split => // v vX; apply: yu. apply: (@setU_i _ (lo_bounds r (singleton v))). by apply: Exercise1_15a18a => //; apply: Xsr. apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)