proposition: Lemma Exercise1_15a11: ~ (has_least r) -> least (completion_order r) emptyset.
proof: Proof. move=> nle. have [oc sr] := Exercise1_15aux. have te: inc emptyset (completion r). apply: Zo_i; first by apply /setP_P; fprops. symmetry;apply /set0_P; move=> y; dneg yu; exists y. move: yu => /Zo_P [ysr [_ yp]]; split => //. move=> x xst; apply: yp;apply: Zo_i=> //; split => //. by move=> t /in_set0. red;rewrite sr; split => // x xsr;apply /sub_gleP;split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)