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
|
(* $Id$ *)
Require Le.
Require Lt.
Require Plus.
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 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.
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.
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.
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.
Hints Resolve gt_trans_S le_gt_trans gt_le_trans : arith v62.
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_antirefl : (n:nat)~(gt n n).
Proof lt_n_n.
Hints Resolve gt_antirefl : arith v62.
Lemma gt_not_sym : (n,m:nat)(gt n m) -> ~(gt m n).
Proof [n,m:nat](lt_not_sym m n).
Lemma gt_not_le : (n,m:nat)(gt n m) -> ~(le n m).
Proof.
Auto with arith.
Qed.
Hints Resolve gt_not_sym gt_not_le : arith v62.
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.
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.
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.
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.
Theorem gt_S : (n,m:nat)(gt (S n) m)->((gt n m)\/(<nat>m=n)).
Proof.
Intros n m H; Unfold gt; Apply le_lt_or_eq; Auto with arith.
Qed.
Theorem gt_O_eq : (n:nat)((gt n O)\/(<nat>O=n)).
Proof.
Intro n ; Apply gt_S ; Auto with arith.
Qed.
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.
|
