proposition: Lemma Exercise1_15a13: greatest (completion_order r) (substrate r).
proof: Proof. have sc: (inc (substrate r) (completion r)). apply: Zo_i; first by aw; apply :setP_Ti. apply: extensionality; [ apply: Exercise1_15a4; fprops | apply: Zo_S]. red; rewrite /completion_order; rewrite (proj2 (sub_osr _)). by split => // x xr; apply /sub_gleP;split => //; move: xr =>/Zo_P [] /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)