proposition: Lemma Exercise1_15a14 X: sub X (completion r) -> least_upper_bound (completion_order r) X (uplo_bounds r (union X)).
proof: Proof. move=> Xc. have [oc sr] := Exercise1_15aux. set (v := uplo_bounds r (union X)). have vc:inc v (completion r). apply: Exercise1_15a7 => t /setU_P [y ty yX]. by move: (Xc _ yX) => /Zo_P [] /setP_P ysr _; apply: ysr. move: (Xc);rewrite - sr => Xc';apply /(lubP oc Xc'); split. split; first (by ue); move=> y yX; rewrite /completion_order; aw. apply /sub_gleP;split => //; first by apply:Xc. by move:(Xc _ yX) => /Zo_P [ysr] ->; apply: Exercise1_15a3; apply: setU_s1. move=> z []; rewrite sr => zc h; rewrite /completion_order; aw. move: zc => /Zo_P [] /setP_P zr ->; rewrite /v. apply /sub_gleP;split;fprops; first by apply: Exercise1_15a7. apply: Exercise1_15a3 => t /setU_P [y ty yX]. by move: (h _ yX) => /sub_gleP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)