proposition: Lemma BRsum_le2r a b c: realp a -> realp b -> realp c -> (a +r c <=r b +r c <-> a <=r b).
proof: Proof. move => ar br cr; split; last first. move:(RSs ar cr)(RSs br cr) => Ha Hb. move => [_ _ sba]; split => // t /BR_sump [u ub [v vc ->]]. apply/BR_sump; exists u; [ by apply:sba | ex_tac ]. move=>[ha hb hc]; split => // t tb. move /BR_P:(cr) => [pa pb cp pd pe]. move /BR_P:(ar) => [pa' pb' pc' pd' pe']. move /BR_P:(br) => [pa'' _ _ _ pe'']. move:(pe'' _ tb) => [t' t'b ltt']. move: (pa'' _ tb)(pa'' _ t'b) => tq t'q. have dp: inc (t -q t') BQps by apply/ qlt0xP; apply / qlt_diffP1. move: (BRi_lowbound cr dp) => [y yc hw]. have: (inc (t' +q y) (b +r c)) by apply/BR_sump; ex_tac; ex_tac. move/hc => /BR_sump [u za [v vc eq]]. have uq: ratp u by apply: pa'. have vq: ratp v by apply: pa. have yq: ratp y by apply: pa. have otq: ratp (BQopp t) by apply: QSo. have utq :ratp (u +q BQopp t) by apply:QSs. have vutq: ratp (v +q (u +q BQopp t)) by apply: QSs. move: (hw _ vc);rewrite BQdiff_diff // - BQsumA // (BQsumC _ t') BQsumA //. rewrite (BQsumC y) eq (BQsumC u) - BQsumA //; move / (qgt_diffP vutq vq). by rewrite BQdiff_sum //; move / (qgt_diffP uq tq); apply: pd'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)