proposition: Lemma Exercise1_2j 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, inc x (substrate r ) -> inc y (substrate r) -> ((gle r x y -> gle r' (class s x) (class s y)) /\ (glt r' (class s x) (class s y) -> glt r x y)).
proof: Proof. move=> woc qoa tor r' x y xsr ysr. move: (Exercise1_2h woc qoa tor) => [tqor _]. move: tor woc => [or tor'] [[ps es sr] woc']. have aux : forall x y,gle r x y -> gle r' (class s x) (class s y). move=> a b ab; apply /quotient_orderP. move: (arg1_sr ab) (arg2_sr ab). rewrite - sr => asr bsr; split => //; try apply: inc_class_setQ => //. move=> c /(class_P es) ac. by move: (woc' _ _ _ ab ac) => [d bd cd]; exists d=> //; apply /(class_P es). split; first by apply: aux => //. move=> [h1 nc]; split; last by dneg xy; ue. case: (tor' _ _ xsr ysr) => // xy; move: (aux _ _ xy) => h2. case: nc; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)