proposition: Theorem div_mult_lt : forall m n p : nat, 0 < n -> 0 < p -> div (p * m) n < p * (1 + div m n).
proof: Proof. intros m n p H H1; apply lt_mult_right_anti with (z := n). apply Nat.le_lt_trans with (p * m). apply div_le; auto. replace (n * (p * (1 + div m n))) with (p * (n * (1 + div m n))); [ idtac | repeat rewrite Nat.mul_assoc; rewrite (Nat.mul_comm p); auto ]. apply mult_lt_bis; try apply div_lt; auto. Qed.
imports: Coq(ArithRing) Bertrand(Misc)