proposition: Lemma qlt_diffP2 a b: ratp a -> ratp b -> (a <q b <-> inc (a -q b) BQms).
proof: Proof. move => pa pb; apply: (iff_trans (qlt_diffP pa pb)). rewrite - (BQoppB pb pa); split => h. by apply: BQopp_positive1. rewrite - (BQopp_K (QS_diff pb pa)); apply: (BQopp_negative1 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)