blob: 4b92881c4f8e69d7863dfa295068eed54658a52f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
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.
|
