proposition: Lemma ltZ_pmul2r m n1 n2 : 0 < m -> (n1 * m < n2 * m) <-> (n1 < n2).
proof: Proof. by move=> ?; split; [exact/Zmult_gt_0_lt_reg_r/Z.lt_gt|exact/Zmult_lt_compat_r]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia