proposition: Lemma BRprod_Mltltge0 a b c d: inc a BRp -> inc c BRp -> a <r b -> c <r d -> (a *r c) <r (b *r d).
proof: Proof. move => pa pb pc pd. have H: (forall a b, inc a BRp -> a <r b -> inc b BRps). move => u v / rle0xP sa sb; apply/ rlt0xP; BRo_tac. move: (H _ _ pa pc) (H _ _ pb pd) => bp cp. case: (equal_or_not c \0r) => cnz. by rewrite cnz BRprod_0r; apply / rlt0xP; apply: RpsS_prod. by apply: BRprod_Mltltgt0 => //; apply/ BRps_iP;split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)