proposition: Theorem div_mult_lt2 : forall m n p : nat, 0 < n -> div (2 * m) n <= 2 * div m n + 1.
proof: Proof. intros m n p H. apply Nat.lt_succ_r. replace (S (2 * div m n + 1)) with (2 * (1 + div m n)); [ apply div_mult_lt | repeat (rewrite <- plus_n_O || rewrite <- plus_n_Sm; simpl in |- *) ]; auto. Qed.
imports: Coq(ArithRing) Bertrand(Misc)