proposition: Lemma BRsum_lt2l a b c: realp a -> realp b -> realp c -> (c +r a <r c +r b <-> a <r b).
proof: Proof. move => ar br cr. apply: (iff_trans (rlt_diffP (RSs cr ar) (RSs cr br))). apply: iff_sym;apply: (iff_trans (rlt_diffP ar br)). by rewrite BRdiff_sum_simpl_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)