proposition: Lemma Exercise1_15a15 X: sub X (completion r) -> nonempty X -> greatest_lower_bound (completion_order r) X (uplo_bounds r (intersection X)).
proof: Proof. move=> Xc neX. have [oc sr] := Exercise1_15aux. set (v := uplo_bounds r (intersection X)). have vc: (inc v (completion r)). move: neX => [x xX]; move: (Xc _ xX) =>/Zo_P [] /setP_P xsr _. apply: Exercise1_15a7 => t ti; move: (setI_hi ti xX); apply: xsr. move: (Xc);rewrite - sr => Xc';apply /(glbP oc Xc'); split. split; first (by ue); move=> y yX; rewrite /completion_order; aw. move:(Xc _ yX) => /Zo_P [] /setP_P ysr ->. apply /sub_gleP;split => //; first by apply : Exercise1_15a7. by apply: Exercise1_15a3; apply :setI_s1. move=> z []; rewrite sr => zc h; apply /sub_gleP; split => //. move: zc => /Zo_P [] /setP_P zr ->. apply: Exercise1_15a3 => t tz; apply: (setI_i neX). by move => y yX; move: (h _ yX) => /sub_gleP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)