proposition: Lemma qlt_diffP a b: ratp a -> ratp b -> (a <q b <-> inc (b -q a) BQps).
proof: Proof. move => pa pb; split. move => [] /(qle_diffP pa pb) => pc pd; apply /BQps_iP;split => //. dneg aux; symmetry; exact (BQdiff_xx_rw pb pa aux). move /BQps_iP => [] /(qle_diffP pa pb) pc pd; split => //. by dneg aux; rewrite aux (BQdiff_xx pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)