proposition: Lemma Exercise1_15a16: complete_lattice (completion_order r).
proof: Proof. apply: Exercise1_11b; first by rewrite /completion_order; fprops. rewrite {1} /completion_order (proj2(sub_osr _)). by move=> X Xsr; exists (uplo_bounds r (union X)); apply:Exercise1_15a14. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)