proposition: Lemma Exercise1_15a12 : has_least (completion_order r).
proof: Proof. case: (p_or_not_p (has_least r)). by move=> [e le]; exists (singleton e); apply: Exercise1_15a10. by exists emptyset; apply: Exercise1_15a11. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)