proposition: Lemma BRsum_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 => xq yq. rewrite (BR_sumQ_aux xq (RS_of_Q yq)). set_extens t. move => /funI_P [z /Zo_P [zq yz] -> ]; apply/Zo_P; split; first by apply:QSs. by apply/BQsum_lt2l. move/Zo_P => [tQ lt]; apply/funI_P; exists (t -q x). move/(BQsum_lt2l (proj31_1 lt) tQ (QSo xq)): lt. rewrite BQsumC -/(_ -q _) (BQdiff_sum xq yq) (BQsumC _ t) => lt1. apply/Zo_P; split => //; apply: (proj32_1 lt1). by rewrite BQsum_diff. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)