proposition: Lemma BRdiff_cQ x y: ratp x -> ratp y -> BR_of_Q x -r BR_of_Q y = BR_of_Q (x -q y).
proof: Proof. move => xr yr. by rewrite /BRdiff (BRopp_Q yr) (BRsum_cQ xr (QSo yr)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)