proposition: Lemma BQsum_le2r a b c: ratp a -> ratp b -> ratp c -> ((a +q c) <=q (b +q c) <-> a <=q b).
proof: Proof. rewrite (BQsumC a c) (BQsumC b c); apply: BQsum_le2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)