From 7e00447c512b71543cec6b6fd63ec44106dada3d Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 24 Jun 2011 15:50:12 +0000 Subject: Numbers: a particular case of div_unique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14238 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/ZMicromega.v | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) (limited to 'plugins/micromega/ZMicromega.v') 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. -- cgit v1.2.3