proposition: Lemma BRsum_opp_r x: realp x -> x +r (BRopp x) = \0r.
proof: Proof. move => xr. case/BR_rational_dichot:(xr) => rx. move/BR_of_Q_prop2:rx => [a aq ->]. by rewrite (BRopp_Q aq) (BRsum_cQ aq (QSo aq)) BQsum_opp_r. rewrite (BRopp_irrational rx). set_extens t. move/BR_sump => [a ax [b /funI_P [c /setC_P [cq ncx] ->] ->]]. move:(BRi_sQ xr ax) => aq; apply/Zo_P; split; first by apply:QS_diff. apply/(qlt_diffP1 cq aq); case:(qleT_ell aq cq) => // sa; case: ncx; try ue. exact:(BRi_segment xr ax sa). move => /Zo_P [tq / qlt0xP tp]. have [a ax h]:=(BRi_lowbound xr tp). have aq:= (BRi_sQ xr ax). apply /BR_sump; ex_tac; exists (t -q a); last by rewrite BQsum_diff. apply /funI_P; exists (a -q t); last by rewrite BQoppB. by have ha:=(QS_diff aq tq); apply /setC_P; split => //; move/h => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)