proposition: Lemma compatibility_proj_increasing r s: preorder_quo_axioms r s -> (weak_order_compatibility r s <-> increasing_pre (canon_proj s) r (quotient_order r s)).
proof: Proof. move=> ax; move: (quotient_is_preorder ax) => pq. have [pr es sr] := ax. rewrite /increasing_pre - sr substrate_quotient_order //; aw. have gs: sgraph s by fprops. split. move=> [_ woc]; split;fprops; first by split; aww. move=> x y lexy. move:(arg1_sr lexy) (arg2_sr lexy); rewrite - sr => xss yss. apply /quotient_orderP; rewrite /quotient_order_r !canon_proj_V //. split;fprops. move=> z /(class_P es) /(woc _ _ _ lexy) [y' /(class_P es) syy' rzy'];ex_tac. move=>[fc [_ _ _ _ ci]]; split => //. move=> x y x' rxy /(class_P es) sxx'. move:(arg1_sr rxy) (arg2_sr rxy); rewrite - sr => xss yss. move /quotient_orderP:(ci _ _ rxy) => [_ _]. rewrite /quotient_order_r !canon_proj_V// => h. by move: (h _ sxx') => [y'] /(class_P es) pa pb; exists y'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)