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