proposition: Lemma BR_sumQ_aux x y: ratp x -> realp y -> (BR_of_Q x) +r y = fun_image y (fun z => x +q z).
proof: Proof. move => xq /BR_P [qa _ _ qd qe]; set_extens t. move => /BR_sump [z /Zo_P [zq xz] [u ub ->]]; apply /funI_P. move:(qa _ ub) => uq. move/(BQsum_lt2l xq zq uq): xz => xw. move/ (BQsum_lt2r (proj31_1 xw) (proj32_1 xw) (QSo xq)): xw. rewrite -/(_ -q _) (BQdiff_sum1 xq uq)(BQsumC u) => ww. have zuq:=(QSs zq uq). by exists ((z +q u) -q x); [ apply:(qd _ _ ub) | rewrite BQsum_diff //]. move /funI_P => [z / qe [u uy l1] ->]; apply/BR_sump. move: (proj31_1 l1) (proj32_1 l1) => uq zq. move/ (BQsum_lt2l uq zq xq):l1 => l2. move/ (BQsum_lt2r (proj31_1 l2) (proj32_1 l2) (QSo uq)):l2. rewrite -/( _ -q _) (BQdiff_sum1 uq xq) => l3. move:(proj32_1 l3)=> l4. exists ( (x +q z) -q u); first by apply/Zo_P. by ex_tac; rewrite BQsum_diff1 //; apply:QSs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)