proposition: Lemma leZ_pmul2l m n1 n2 : 0 < m -> m * n1 <= m * n2 <-> (n1 <= n2).
proof: Proof. move=> m0; split; first by rewrite !(mulZC m); exact: Zmult_lt_0_le_reg_r. by move/Zmult_le_compat_l; apply; exact/ltZW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia