proposition: Lemma BQsum_same_den x y: ratp x -> ratp y -> Qden x = Qden y -> x +q y = BQ_of_pair (Qnum x +z Qnum y) (Qden x).
proof: Proof. move => /BQ_P [_ nx dxp cp] /BQ_P [_ ny dyp cy] h. have dx:= (BZps_sBZ dxp). have dxy := (ZpsS_prod dxp dxp). have nxy := (ZSs nx ny). rewrite /BQsum - h (BZprodC (Q x)) - BZprodDl //. apply/(BQ_of_pair_prop5 (ZSp (ZSs nx ny) dx) dxy nxy dxp). by rewrite - (BZprodA nxy dx dx) BZprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)