proposition: Lemma Exercise1_2g r s: weak_order_compatibility r s-> Ex1_2_hC' r s -> total_order r -> let r' := (quotient_order r s) in forall x y, gle r' x y <-> [/\ inc x (quotient s) , inc y (quotient s)& gle r (rep x) (rep y)].
proof: Proof. move=> [[ps es sr] woc] qoa [or tor] r' x y. have ru: (forall u, inc u (quotient s) -> inc (rep u) u). by move=> u uq; apply: (setQ_repi es uq). split. move /quotient_orderP=> [xq yq etc]; split => //. move: (ru _ xq) (ru _ yq) => rxx ryy. have rxs: (inc (rep x) (substrate r)) by rewrite - sr; fprops. have rys: (inc (rep y) (substrate r)) by rewrite - sr; fprops. case: (tor _ _ rys rxs) => // crxy. move: (etc _ rxx) => [z zy rz]. have ryz: (gle r (rep y) z) by order_tac. have syz: (related s (rep y) z). by apply /(rel_in_class es _ zy); apply /(setQ_P es). by move: (qoa _ _ _ crxy rz syz) =>/(related_rr_P es yq xq) ->; order_tac. move => [xq yq rr]. apply /quotient_orderP;split => // u ux. move: (ru _ xq) (ru _ yq) => rxx ryy. have rrux: (related s (rep x) u). by apply /(rel_in_class es _ ux); apply /(setQ_P es). move: (woc _ _ _ rr rrux)=> [v v1 v2]; exists v => //. by apply: (rel_in_class2 es _ v1); apply /(setQ_P es). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)