proposition: Lemma Exercise1_2d r s: equivalence s -> order r -> substrate s = substrate r -> Ex1_2_hC' r s -> order (quotient_order r s).
proof: Proof. move => es or ss qoa. have pr:= (order_preorder or). have pqa: preorder_quo_axioms r s by []. have [p1 p2 p3] := (quotient_is_preorder pqa). split => //. suff sxy: forall x y, related (quotient_order r s) x y -> related (quotient_order r s) y x -> sub x y. by move=> x y xs ys; apply: extensionality; apply: sxy. move=> x y /quotient_orderP [xs ys q1] /quotient_orderP [_ _ q2] t tx. move: (q1 _ tx) => [z zy tz]; move: (q2 _ zy) => [w wt zw]. have tw: (related s t w). by apply /(in_class_relatedP es); exists x; split => //; apply /(setQ_P es). rewrite (is_class_pr es zy ys);apply /(class_P es); apply: (symmetricity_e es). exact: (qoa _ _ _ tz zw tw). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)