proposition: Lemma BQsum_div a b c: ratp a -> ratp b -> ratp c -> c <> \0q -> a +q (b /q c) = (a *q c +q b) /q c.
proof: Proof. move => aq bq cq cnz; move:(QS_inv cq) => icq. have {1} -> : a = (a *q c) /q c by rewrite BQprodC BQdiv_prod //. by rewrite - BQprodDl //; apply: QSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)