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
150
151
152
153
154
155
156
157
158
|
(************************************************************************)
(* 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$ i*)
(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
<<
Definition gt (n m:nat) := m < n.
>>
*)
Require Import Le.
Require Import Lt.
Require Import Plus.
Open Local Scope nat_scope.
Implicit Types m n p : nat.
(** * Order and successor *)
Theorem gt_Sn_O : forall n, S n > 0.
Proof.
auto with arith.
Qed.
Hint Resolve gt_Sn_O: arith v62.
Theorem gt_Sn_n : forall n, S n > n.
Proof.
auto with arith.
Qed.
Hint Resolve gt_Sn_n: arith v62.
Theorem gt_n_S : forall n m, n > m -> S n > S m.
Proof.
auto with arith.
Qed.
Hint Resolve gt_n_S: arith v62.
Lemma gt_S_n : forall n m, S m > S n -> m > n.
Proof.
auto with arith.
Qed.
Hint Immediate gt_S_n: arith v62.
Theorem gt_S : forall n m, S n > m -> n > m \/ m = n.
Proof.
intros n m H; unfold gt in |- *; apply le_lt_or_eq; auto with arith.
Qed.
Lemma gt_pred : forall n m, m > S n -> pred m > n.
Proof.
auto with arith.
Qed.
Hint Immediate gt_pred: arith v62.
(** * Irreflexivity *)
Lemma gt_irrefl : forall n, ~ n > n.
Proof lt_irrefl.
Hint Resolve gt_irrefl: arith v62.
(** * Asymmetry *)
Lemma gt_asym : forall n m, n > m -> ~ m > n.
Proof fun n m => lt_asym m n.
Hint Resolve gt_asym: arith v62.
(** * Relating strict and large orders *)
Lemma le_not_gt : forall n m, n <= m -> ~ n > m.
Proof le_not_lt.
Hint Resolve le_not_gt: arith v62.
Lemma gt_not_le : forall n m, n > m -> ~ n <= m.
Proof.
auto with arith.
Qed.
Hint Resolve gt_not_le: arith v62.
Theorem le_S_gt : forall n m, S n <= m -> m > n.
Proof.
auto with arith.
Qed.
Hint Immediate le_S_gt: arith v62.
Lemma gt_S_le : forall n m, S m > n -> n <= m.
Proof.
intros n p; exact (lt_n_Sm_le n p).
Qed.
Hint Immediate gt_S_le: arith v62.
Lemma gt_le_S : forall n m, m > n -> S n <= m.
Proof.
auto with arith.
Qed.
Hint Resolve gt_le_S: arith v62.
Lemma le_gt_S : forall n m, n <= m -> S m > n.
Proof.
auto with arith.
Qed.
Hint Resolve le_gt_S: arith v62.
(** * Transitivity *)
Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p.
Proof.
red in |- *; intros; apply lt_le_trans with m; auto with arith.
Qed.
Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p.
Proof.
red in |- *; intros; apply le_lt_trans with m; auto with arith.
Qed.
Lemma gt_trans : forall n m p, n > m -> m > p -> n > p.
Proof.
red in |- *; intros n m p H1 H2.
apply lt_trans with m; auto with arith.
Qed.
Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p.
Proof.
red in |- *; intros; apply lt_le_trans with m; auto with arith.
Qed.
Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
(** * Comparison to 0 *)
Theorem gt_0_eq : forall n, n > 0 \/ 0 = n.
Proof.
intro n; apply gt_S; auto with arith.
Qed.
(** * Simplification and compatibility *)
Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m.
Proof.
red in |- *; intros n m p H; apply plus_lt_reg_l with p; auto with arith.
Qed.
Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
Proof.
auto with arith.
Qed.
Hint Resolve plus_gt_compat_l: arith v62.
(* begin hide *)
Notation gt_O_eq := gt_0_eq (only parsing).
(* end hide *)
|
