proposition: Lemma Exercise1_15c r: total_order r -> total_order (completion_order r).
proof: Proof. move: (sub_osr (completion r)) => [pa pb] [or tor]. split => //; rewrite pb => x y xc yc. have aux: (forall x a b, inc x (completion r) -> inc a x -> gle r b a -> inc b x). move=> v a b /Zo_P [vsr hv]. rewrite hv => /Zo_P [asr [_ lb]] ab; apply: Zo_i; first by order_tac. split; [ by order_tac | move=> w wl; move: (lb _ wl) => aw; order_tac ]. case: (p_or_not_p (sub x y)) => h; [left | right]; apply /sub_gleP;split => //. move => t ty; ex_middle tx; case: h; move=> z zx; ex_middle zy. have tsr: inc t (substrate r) by move: yc =>/Zo_P [] /setP_P ysr _; apply: ysr. have zsr: inc z (substrate r) by move: xc =>/Zo_P [] /setP_P ysr _; apply: ysr. case: (tor _ _ tsr zsr) => ctz. case: tx; exact: (aux _ _ _ xc zx ctz). exact: (aux _ _ _ yc ty ctz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)