proposition: Lemma strong_order_compatibility r s: preorder_quo_axioms r s -> Ex1_2_strong_l r s -> weak_order_compatibility r s.
proof: Proof. move=> h1 h2; split => //. move: h1 => [po eq ss] x y x' xy sxx'; exists y; last by apply: h2 xy sxx'. apply: reflexivity_e => //;red in xy;rewrite ss; substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)