proposition: Lemma qltP x y: x <q y <-> [/\ ratp x, ratp y & (Qnum x) *z (Qden y) <z (Qden x) *z (Qnum y) ].
proof: Proof. split. move => [[xq yq le1] xny]; split => //; split => //; dneg h. apply: qleA; split => //. rewrite /BQle_aux in le1. rewrite /BQle_aux (BZprodC (Q y)) h BZprodC; apply: zleR; BZo_tac. by move => [xq yq [le1 lt1]]; split => //; dneg h; rewrite h BZprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)