proposition: Lemma Exercise1_2h r s: weak_order_compatibility r s-> Ex1_2_hC' r s -> total_order r -> total_order (quotient_order r s).
proof: Proof. move=> woc qoa tor. move: (Exercise1_2g woc qoa tor) => e2g. move: (woc) tor => [[ps es sr] woc'] [or tor]. move: (Exercise1_2d es or sr qoa) => oqo; split => //. rewrite substrate_quotient_order //. move=> x y xq yq. have rx: (inc (rep x) (substrate r)) by rewrite - sr; apply: rep_i_sr. have ry: (inc (rep y) (substrate r)) by rewrite - sr; apply: rep_i_sr. by case: (tor _ _ rx ry) => h; [left | right]; rewrite e2g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)