proposition: Lemma leZ_pmul2r m n1 n2 : 0 < m -> n1 * m <= n2 * m <-> (n1 <= n2).
proof: Proof. move=> m0; split; first by apply: Zmult_le_reg_r; apply Z.lt_gt. by move=> *; apply leZ_wpmul2r => //; exact: ltZW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia