proposition: Lemma BR_sumQ_aux1 x y: rationalp x -> irrationalp y -> irrationalp (x +r y).
proof: Proof. move => xra [/BR_P yr yi]; split. apply/BR_P;apply:RSs => //; apply/BR_P; exact: (proj1 xra). move/BR_of_Q_prop2:xra => [a aq ->]. rewrite (BR_sumQ_aux aq yr) => t /setC_P [tq] /funI_P h. case: (inc_or_not (t -q a) y) => tay. by case:h; ex_tac; rewrite BQsum_diff. move:(yi _ (setC_i (QS_diff tq aq) tay)) => [b /setC_P [bq bb] bc]. move/(BQsum_lt2l (proj31_1 bc) bq aq): bc; rewrite (BQsum_diff aq tq) => lt. exists (a+q b) => //; apply /setC_P;split; first by rewrite -/(ratp _);BQo_tac. move => /funI_P [z zy]. by move/(BQsum_eq2l aq bq (BRi_sQ yr zy)) => bz; case:bb; rewrite bz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)