proposition: Lemma BRsum_Mltge0 a c d: a <r c -> \0r <=r d -> a <r (c +r d).
proof: Proof. by move => pa pb; move: (BRsum_Mltle pa pb); rewrite (BRsum_0r (proj31_1 pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)