proposition: Lemma qgt_diffP a b: ratp a -> ratp b -> (a -q b <q \0q <-> a <q b).
proof: Proof. move => aq bq; rewrite - (BQoppB bq aq). apply:iff_sym;apply: (iff_trans(qlt_diffP aq bq)); split. by move => /BQopp_positive1 / qgt0xP. by move/ qgt0xP => /BQopp_negative1; rewrite BQopp_K //; apply:QS_diff. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)