3 files changed, 32 insertions, 0 deletions
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