proposition: Lemma BRsquare_mon2 x y: inc x BRp -> inc y BRp -> BRsquare x <=r BRsquare y -> x <=r y.
proof: Proof. move => ha hb hc; case: (rleT_el (BRp_sBR ha)(BRp_sBR hb)) => // hd. move: (BRprod_Mltltge0 hb hb hd hd) => he; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)