proposition: Lemma RpsS_sum_r x y: inc x BRp -> inc y BRps -> inc (x +r y) BRps.
proof: Proof. move => xp yps; move: (BRps_sBRp yps) => yp. apply/setC_P; split; first by apply:RpS_sum. move/set1_P /(BRsum_opp_rev (BRp_sBR xp) (BRp_sBR yp)) => h. move:(BRopp_positive1 yps); rewrite -h => ha. exact:(BR_di_neg_pos ha xp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)