proposition: Theorem div_unique : forall m n p : nat, 0 < n -> n * p <= m -> m < n * (1 + p) -> p = div m n.
proof: Proof. intros m n p H H0 H1. case (Nat.le_gt_cases p (div m n)); intros H2. case ((proj1 (Nat.lt_eq_cases _ _)) H2); intros H3; auto. absurd (n * div m n <= m). apply Nat.lt_nge; apply Nat.lt_le_trans with (1 := H1); auto with arith. apply div_le; auto. absurd (m < n * (1 + div m n)). apply Nat.le_ngt; apply Nat.le_trans with (2 := H0); auto with arith. apply div_lt; auto. Qed.
imports: Coq(ArithRing) Bertrand(Misc)