proposition: Lemma Exercise1_15a10 e: least r e -> least (completion_order r) (singleton e).
proof: Proof. move=> [es le]. have [oc sr] := Exercise1_15aux. have sse: (sub (singleton e) (substrate r)) by move => t /set1_P ->. have se: inc (singleton e) (completion r). apply: Zo_i; first by apply /setP_P. apply: extensionality; first by apply: Exercise1_15a4. move=> t /Zo_P [tsr [_ h]]; apply /set1_P. apply: (order_antisymmetry or); last by apply: le. by apply: h; apply: Zo_i => //; split => // y /set1_P ->; order_tac. red; rewrite sr; split => //. move=> x xr; apply /sub_gleP;split => // s /set1_P ->. move: xr => /Zo_P [] /setP_P h ->; apply: Zo_i => //. by split => //; move=> y => /Zo_P [ ysr _]; apply: le. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)