proposition: Lemma Exercise1_15aux: order_on (completion_order r)(completion r).
proof: Proof. rewrite/order_on/completion_order; split; fprops. by rewrite (proj2(sub_osr _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)