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