1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id: Gt.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
Require Le.
Require Lt.
Require Plus.
V7only [Import nat_scope.].
Open Local Scope nat_scope.
Implicit Variables Type m,n,p:nat.
(** Order and successor *)
Theorem gt_Sn_O : (n:nat)(gt (S n) O).
Proof.
Auto with arith.
Qed.
Hints Resolve gt_Sn_O : arith v62.
Theorem gt_Sn_n : (n:nat)(gt (S n) n).
Proof.
Auto with arith.
Qed.
Hints Resolve gt_Sn_n : arith v62.
Theorem gt_n_S : (n,m:nat)(gt n m)->(gt (S n) (S m)).
Proof.
Auto with arith.
Qed.
Hints Resolve gt_n_S : arith v62.
Lemma gt_S_n : (n,p:nat)(gt (S p) (S n))->(gt p n).
Proof.
Auto with arith.
Qed.
Hints Immediate gt_S_n : arith v62.
Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(m=n)).
Proof.
Intros n m H; Unfold gt; Apply le_lt_or_eq; Auto with arith.
Qed.
Lemma gt_pred : (n,p:nat)(gt p (S n))->(gt (pred p) n).
Proof.
Auto with arith.
Qed.
Hints Immediate gt_pred : arith v62.
(** Irreflexivity *)
Lemma gt_antirefl : (n:nat)~(gt n n).
Proof lt_n_n.
Hints Resolve gt_antirefl : arith v62.
(** Asymmetry *)
Lemma gt_not_sym : (n,m:nat)(gt n m) -> ~(gt m n).
Proof [n,m:nat](lt_not_sym m n).
Hints Resolve gt_not_sym : arith v62.
(** Relating strict and large orders *)
Lemma le_not_gt : (n,m:nat)(le n m) -> ~(gt n m).
Proof le_not_lt.
Hints Resolve le_not_gt : arith v62.
Lemma gt_not_le : (n,m:nat)(gt n m) -> ~(le n m).
Proof.
Auto with arith.
Qed.
Hints Resolve gt_not_le : arith v62.
Theorem le_S_gt : (n,m:nat)(le (S n) m)->(gt m n).
Proof.
Auto with arith.
Qed.
Hints Immediate le_S_gt : arith v62.
Lemma gt_S_le : (n,p:nat)(gt (S p) n)->(le n p).
Proof.
Intros n p; Exact (lt_n_Sm_le n p).
Qed.
Hints Immediate gt_S_le : arith v62.
Lemma gt_le_S : (n,p:nat)(gt p n)->(le (S n) p).
Proof.
Auto with arith.
Qed.
Hints Resolve gt_le_S : arith v62.
Lemma le_gt_S : (n,p:nat)(le n p)->(gt (S p) n).
Proof.
Auto with arith.
Qed.
Hints Resolve le_gt_S : arith v62.
(** Transitivity *)
Theorem le_gt_trans : (n,m,p:nat)(le m n)->(gt m p)->(gt n p).
Proof.
Red; Intros; Apply lt_le_trans with m; Auto with arith.
Qed.
Theorem gt_le_trans : (n,m,p:nat)(gt n m)->(le p m)->(gt n p).
Proof.
Red; Intros; Apply le_lt_trans with m; Auto with arith.
Qed.
Lemma gt_trans : (n,m,p:nat)(gt n m)->(gt m p)->(gt n p).
Proof.
Red; Intros n m p H1 H2.
Apply lt_trans with m; Auto with arith.
Qed.
Theorem gt_trans_S : (n,m,p:nat)(gt (S n) m)->(gt m p)->(gt n p).
Proof.
Red; Intros; Apply lt_le_trans with m; Auto with arith.
Qed.
Hints Resolve gt_trans_S le_gt_trans gt_le_trans : arith v62.
(** Comparison to 0 *)
Theorem gt_O_eq : (n:nat)((gt n O)\/(O=n)).
Proof.
Intro n ; Apply gt_S ; Auto with arith.
Qed.
(** Simplification and compatibility *)
Lemma simpl_gt_plus_l : (n,m,p:nat)(gt (plus p n) (plus p m))->(gt n m).
Proof.
Red; Intros n m p H; Apply simpl_lt_plus_l with p; Auto with arith.
Qed.
Lemma gt_reg_l : (n,m,p:nat)(gt n m)->(gt (plus p n) (plus p m)).
Proof.
Auto with arith.
Qed.
Hints Resolve gt_reg_l : arith v62.
|
