diff options
Diffstat (limited to 'plugins/micromega/ZMicromega.v')
| -rw-r--r-- | plugins/micromega/ZMicromega.v | 12 |
1 files changed, 1 insertions, 11 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. |