proposition: Theorem div_lt : forall m n : nat, 0 < n -> m < n * (1 + div m n).
proof: Proof. intros m n H; unfold div in |- *; generalize (pdiv_def m n H); case (pdiv m n); simpl in |- *. intros q r (H1, H2); rewrite H1; auto with arith. rewrite (Nat.mul_comm n); simpl in |- *; auto with arith. rewrite (Nat.add_comm n); simpl in |- *; auto with arith. Qed.
imports: Coq(ArithRing) Bertrand(Misc)