proposition: Lemma BZprod_ple2r a b c: intp a -> intp b -> inc c BZps -> ((a *z c) <=z (b *z c) <-> a <=z b).
proof: Proof. move => pa pb pc; move: (BZps_sBZp pc)=> p'c. split; last by apply:BZprod_Mlege0. move => h; case: (zleT_el pa pb) => // h1. move: (BZprod_Mltgt0 pc h1) => h2; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)