proposition: Lemma quotient_orderP r s x y: related (quotient_order r s) x y <-> quotient_order_r r s x y.
proof: Proof. split; [by move /Zo_hi; aw | move => h; move: (h) => [pa pb _] ]. by apply: Zo_i; aw; trivial; apply /setXp_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)