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