proposition: Lemma Zmult_le_reg_l : forall m n p, 0 < p -> p * m <= p * n -> m <= n.
proof: Proof. intros m n p p_pos ; do 2 rewrite (Zmult_comm p) ; apply Zmult_le_reg_r, Z.lt_gt ; assumption. Qed.
imports: ZArith Znumtheory Lia Zpow_facts MyZ Hurwitz_def