From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/QArith/Qround.v | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'theories/QArith/Qround.v')

diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 01a97870..ce363a33 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -136,4 +136,15 @@ intros x y H.
 apply Zle_antisym.
  auto with *.
 symmetry in H; auto with *.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m).
+Proof.
+ unfold Qfloor. intros. simpl.
+ destruct m as [?|?|p]; simpl.
+  now rewrite Zdiv_0_r, Zmult_0_r.
+  now rewrite Zmult_1_r.
+ rewrite <- Zopp_eq_mult_neg_1.
+ rewrite <- (Zopp_involutive (Zpos p)).
+ now rewrite Zdiv_opp_opp.
+Qed.
-- 
cgit v1.2.3