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