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