From 362ccc063fa14ee0dbec6f25f1d4c45eca11013a Mon Sep 17 00:00:00 2001
From: roconnor
Date: Tue, 5 Feb 2008 10:47:51 +0000
Subject: Add Morphisms for Qceiling and Qfloor

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10508 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/QArith/Qabs.v   |  8 ++++++++
 theories/QArith/Qpower.v |  8 ++++++++
 theories/QArith/Qround.v | 16 ++++++++++++++++
 3 files changed, 32 insertions(+)

diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index b3f5e7af48..e672016e84 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Export QArith.
 Require Export Qreduction.
 
diff --git a/theories/QArith/Qpower.v b/theories/QArith/Qpower.v
index 54cf4bcbd8..78034802fa 100644
--- a/theories/QArith/Qpower.v
+++ b/theories/QArith/Qpower.v
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 Require Import Zpow_facts Qfield Qreduction.
 
 Lemma Qpower_positive_1 : forall n, Qpower_positive 1 n == 1.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 2479c2259f..8162a702fa 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -121,3 +121,19 @@ cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *.
 Qed.
 
 Hint Resolve Qceiling_resp_le : qarith.
+
+Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.
+Proof.
+intros x y H.
+apply Zle_antisym.
+ auto with *.
+symmetry in H; auto with *.
+Qed.
+
+Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp.
+Proof.
+intros x y H.
+apply Zle_antisym.
+ auto with *.
+symmetry in H; auto with *.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3