proposition: Theorem Zmult_interval: forall p q, 0 < p * q -> 1 < p -> 0 < q < p * q.
proof: Proof. intros p q H1 H2; assert (0 < q). case (Zle_or_lt q 0); auto; intros H3; contradict H1; apply Zle_not_lt. rewrite <- (Zmult_0_r p). apply Zmult_le_compat_l; auto with zarith. split; auto. pattern q at 1; rewrite <- (Zmult_1_l q). apply Zmult_lt_compat_r; auto with zarith. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic