proposition: Lemma RSs x y: realp x -> realp y -> realp (x +r y).
proof: Proof. move => /BR_P [pa pb pc pd pe] /BR_P [qa qb qc qd qe]. apply/BR_P; split. + by move => t/BR_sump [z za [u ua ->]]; apply:QSs; [apply:pa | apply:qa]. + move:pb qb => [a ax] [b iby]; exists (a +q b); apply/BR_sump. ex_tac; ex_tac. + move => h. move:(setC_ne (conj pa pc)) => [a /setC_P [aq anx]]. move:(setC_ne (conj qa qc)) => [b /setC_P [bq bnx]]. move:(QSs aq bq); rewrite /ratp -h; move => /BR_sump [z za [u ua zv]]. case: (qleT_ell (pa _ za) aq) => l1;first by case: anx; rewrite - l1. by move:(pd _ _ za l1). case: (qleT_ell (qa _ ua) bq) => l2;first by case: bnx; rewrite - l2. by move:(qd _ _ ua l2). by move: (proj2 (BQsum_Mltlt l1 l2)); rewrite zv. + move => a b /BR_sump [z za [u ua zv]] l1; apply/BR_sump. move:(qa _ ua) (pa _ za)(proj32_1 l1) => uq zq bq. have aux: inc (b -q u) x. apply: (pd _ _ za); rewrite -(BQdiff_sum uq zq) BQsumC - zv. apply /BQsum_lt2r => //; [ BQo_tac | by apply:QSo]. by ex_tac; ex_tac; rewrite (BQsum_diff1 uq bq). + move =>a /BR_sump [z /pe [b bx bv] [u ua zv]]. move: (qa _ ua) (pa _ bx)(proj32_1 bv) => uq bq zq. have aux: b +q u <q a by rewrite zv; apply/BQsum_lt2r. exists (b +q u) => //;apply/BR_sump; ex_tac; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)