proposition: Lemma RmsS_sum_rl x y: inc x BRms -> inc y BRms -> inc (x +r y) BRms.
proof: Proof. move => xr yr. move: (BRopp_negative1 xr) (BRopp_negative1 yr) => xr1 yr1. move: (BRms_sBR xr)(BRms_sBR yr) => xr2 yr2. move:(RpsS_sum_rl xr1 yr1); rewrite - (BRoppD xr2 yr2) => h. by move: (BRopp_K (RSs xr2 yr2)) => <-; apply: BRopp_positive1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)