proposition: Lemma qlt_diffP1 a b: ratp a -> ratp b -> (\0q <q (b -q a) <-> a <q b).
proof: Proof. move => pa pb; apply: iff_sym; apply: (iff_trans (qlt_diffP pa pb)). apply:iff_sym ;exact:qlt0xP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)