proposition: Lemma pmulZ_rgt0 x y : 0 < x -> (0 < x * y) <-> (0 < y).
proof: Proof. by move=> x0; split; [rewrite mulZC; apply Zmult_lt_0_reg_r|exact: mulZ_gt0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) ZArith Lia