proposition: Lemma BRsum_le2l a b c: realp a -> realp b -> realp c -> ((c +r a) <=r (c +r b) <-> a <=r b).
proof: Proof. rewrite (BRsumC c) (BRsumC c); apply:BRsum_le2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)