diff options
Diffstat (limited to 'src/Util/ZUtil/Ge.v')
-rw-r--r-- | src/Util/ZUtil/Ge.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Ge.v b/src/Util/ZUtil/Ge.v new file mode 100644 index 000000000..4b92881c4 --- /dev/null +++ b/src/Util/ZUtil/Ge.v @@ -0,0 +1,13 @@ +Require Import Coq.ZArith.ZArith Coq.Classes.RelationClasses. + +Local Open Scope Z_scope. + +Module Z. + Lemma ge_refl x : x >= x. + Proof. rewrite !Z.ge_le_iff; reflexivity. Qed. + Lemma ge_trans n m p : n >= m -> m >= p -> n >= p. + Proof. rewrite !Z.ge_le_iff; eauto using Z.le_trans. Qed. + + Global Instance ge_preorder : PreOrder Z.ge. + Proof. constructor; hnf; [ apply ge_refl | apply ge_trans ]. Defined. +End Z. |