proposition: Lemma Exercise1_15a8 r A: sub A (substrate r) -> inc (lo_bounds r A) (completion r).
proof: Proof. move=> Asr; apply: Zo_i; first by apply /setP_P; apply: Zo_S. rewrite /uplo_bounds Exercise1_15a5 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)