proposition: Lemma ltZ_pmul2r' m n1 n2 : 0 < m -> n1 * m <? n2 * m = (n1 <? n2).
proof: Proof. by move=> H; apply/idP/idP => /ltZP/(ltZ_pmul2r _ _ _ H)/ltZP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia