proposition: Lemma BRsum_Mlelt a b c d: a <=r c -> b <r d -> (a +r b) <r (c +r d).
proof: Proof. move => eq1 eq2; move: (proj32 eq1) (proj31_1 eq2)=> cr br. move /(BRsum_le2r (proj31 eq1) cr br): eq1 => eq3. move/(BRsum_lt2l br (proj32_1 eq2) cr): eq2 => eq4. BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)