aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--plugins/micromega/ZMicromega.v12
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivEucl.v5
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivFloor.v5
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivTrunc.v5
-rw-r--r--theories/Numbers/NatInt/NZDiv.v18
-rw-r--r--theories/Numbers/Natural/Abstract/NDiv.v4
6 files changed, 28 insertions, 21 deletions
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index f840e471b..461f53b54 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -296,16 +296,6 @@ Proof.
reflexivity.
Qed.
-Lemma Zdivide_Zdiv : forall a b c, b <> 0 -> (b | c) -> b * a = c -> a = c / b.
-Proof.
- intros.
- inv H0.
- rewrite H2.
- rewrite Z_div_mult_full ; auto.
- apply Zmult_reg_l with (p :=b) ; auto.
- rewrite (Zmult_comm b q). auto.
-Qed.
-
Lemma narrow_interval_lower_bound : forall a b x, a > 0 -> a * x >= b -> x >= ceiling b a.
Proof.
unfold ceiling.
@@ -780,7 +770,7 @@ Proof.
apply Zdivide_opp_r in H4.
rewrite Zdivide_ceiling ; auto.
apply Zeq_minus.
- apply Zdivide_Zdiv ; auto with zarith.
+ apply Z.div_unique_exact ; auto with zarith.
intros.
unfold nformula_of_cutting_plane.
inv H3.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index e1802dbee..954b89150 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -268,6 +268,11 @@ Proof.
intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
Qed.
+Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b.
+Proof.
+ intros Hb H. rewrite H, mul_comm. symmetry. now apply div_mul.
+Qed.
+
(** * Order results about mod and div *)
(** A modulo cannot grow beyond its starting point. *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index bc1932d44..f19baf4d1 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -316,6 +316,11 @@ Proof.
intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag.
Qed.
+Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b.
+Proof.
+ intros Hb H. rewrite H, mul_comm. symmetry. now apply div_mul.
+Qed.
+
(** * Order results about mod and div *)
(** A modulo cannot grow beyond its starting point. *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 09f9e023e..74abedb42 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -178,6 +178,11 @@ Proof.
intros. rewrite rem_eq, quot_mul by trivial. rewrite mul_comm; apply sub_diag.
Qed.
+Theorem quot_unique_exact a b q: b~=0 -> a == b*q -> q == a÷b.
+Proof.
+ intros Hb H. rewrite H, mul_comm. symmetry. now apply quot_mul.
+Qed.
+
(** The sign of [a rem b] is the one of [a] (when it's not null) *)
Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b.
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index aa7ad824c..bc109aced 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -90,14 +90,17 @@ apply mod_bound_pos; order.
rewrite <- div_mod; order.
Qed.
+Theorem div_unique_exact a b q:
+ 0<=a -> 0<b -> a == b*q -> q == a/b.
+Proof.
+ intros Ha Hb H. apply div_unique with 0; nzsimpl; now try split.
+Qed.
(** A division by itself returns 1 *)
Lemma div_same : forall a, 0<a -> a/a == 1.
Proof.
-intros. symmetry.
-apply div_unique with 0; intuition; try order.
-now nzsimpl.
+intros. symmetry. apply div_unique_exact; nzsimpl; order.
Qed.
Lemma mod_same : forall a, 0<a -> a mod a == 0.
@@ -139,9 +142,7 @@ Qed.
Lemma div_1_r: forall a, 0<=a -> a/1 == a.
Proof.
-intros. symmetry.
-apply div_unique with 0; try split; try order; try apply lt_0_1.
-now nzsimpl.
+intros. symmetry. apply div_unique_exact; nzsimpl; order'.
Qed.
Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0.
@@ -163,10 +164,9 @@ Qed.
Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a.
Proof.
-intros; symmetry.
-apply div_unique with 0; try split; try order.
+intros; symmetry. apply div_unique_exact; trivial.
apply mul_nonneg_nonneg; order.
-nzsimpl; apply mul_comm.
+apply mul_comm.
Qed.
Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0.
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 47f409605..105051611 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -47,6 +47,9 @@ Theorem mod_unique:
forall a b q r, r<b -> a == b*q + r -> r == a mod b.
Proof. intros. apply mod_unique with q; auto'. Qed.
+Theorem div_unique_exact: forall a b q, b~=0 -> a == b*q -> q == a/b.
+Proof. intros. apply div_unique_exact; auto'. Qed.
+
(** A division by itself returns 1 *)
Lemma div_same : forall a, a~=0 -> a/a == 1.
@@ -236,4 +239,3 @@ Lemma mod_divides : forall a b, b~=0 ->
Proof. intros. apply mod_divides; auto'. Qed.
End NDivProp.
-