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