proposition: Lemma Exercise1_15a18: order_morphism (Lf lobs (substrate r) (substrate (completion_order r))) r (completion_order r).
proof: Proof. move: (Exercise1_15a17). rewrite /order_morphism/completion_order (proj2(sub_osr _)) => ta. split => //; first by fprops. saw;apply: lf_function => //. hnf; aw;move=> x y xsr ysr; rewrite !LfV//; split. move => xy; apply /sub_gleP;split;fprops. move=> t /Zo_P [tsr [_ ts]]; apply :Zo_i => //. move: (ts _ (set1_1 x)) => tx. split => // u /set1_P ->; order_tac. move /sub_gleP => [_ _ h]; move: (h _ (Exercise1_15a18a xsr)). move/Zo_hi => [_]; apply; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)