proposition: Lemma BZprod_Mlelege0 a b c d: inc b BZp -> inc c BZp -> a <=z b -> c <=z d -> (a *z c) <=z (b *z d).
proof: Proof. move => pa pb pc pd. move: (BZprod_Mlege0 pb pc) (BZprod_Mlege0 pa pd) => r1. rewrite (BZprodC c) (BZprodC d) => r2; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)