proposition: Lemma BRsquare_mon1 x y: inc x BRp -> inc y BRp -> x <=r y -> BRsquare x <=r BRsquare y.
proof: Proof. move => ha hb hc; exact: (BRprod_Mlelege0 hb ha hc hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)