proposition: Lemma BRprod_Mlelege0 a b c d: inc b BRp -> inc c BRp -> a <=r b -> c <=r d -> (a *r c) <=r (b *r d).
proof: Proof. move => pa pb pc pd. move: (BRprod_Mlege0 pb pc) (BRprod_Mlege0 pa pd) => r1. rewrite (BRprodC c) (BRprodC d) => r2; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)