-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathGraveyard.v
307 lines (258 loc) · 34.8 KB
/
Graveyard.v
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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
Require Import Arith Lia.
(* This is the current contender for largest number. *)
(* Submitted by codyroux *)
Definition contender_0 : nat := 0.
Theorem contender_0_lt_nothing : True.
Proof.
auto.
Qed.
(* Submitted by codyroux *)
Definition contender_1 : nat := 42.
Theorem contender_0_lt_contender_1 : contender_0 < contender_1.
Proof.
unfold contender_0, contender_1.
auto with arith.
Qed.
(* This is the current contender for largest number. *)
(* Submitted by jaykru *)
Time Definition contender_2 : nat := 42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42^42.
Theorem contender_1_lt_contender_2 : contender_1 < contender_2.
Proof.
Time cbv delta [contender_1 contender_2];
repeat match goal with
| _ => progress eapply Nat.pow_lt_mono_r; [solve [lia]|]
| |- ?x < ?y =>
match y with
| context[x ^ x] =>
progress erewrite <-Nat.pow_1_r at 1
end
| _ => progress eapply Nat.pow_gt_1; [solve [lia]|]
| _ => progress eapply Nat.pow_nonzero; solve [lia]
end.
Time Qed.
(** * Solution notes
- Definition time was something like 2 seconds
- Proof script and Qed time altogether were less than a minute, roughly 50 seconds.
*)
(* This is the current contender for largest number *)
(* Submitted by codyroux *)
(* This is a fun trick *)
Opaque Nat.pow.
Definition tower_of_power (n : nat) : nat :=
Nat.recursion 42 (fun _ k => 42 ^ k) n.
Ltac depth t :=
match constr:(t) with
| 42 => constr:(0)
| ?x ^ ?y =>
let d := depth y in
constr:(S d)
| _ => fail
end.
Ltac reify_tower t :=
match constr:(t) with
| _ ^ _ =>
let d := depth t in
constr:(tower_of_power d)
| _ => fail
end.
Ltac reify_goal :=
match goal with
| [ |- ?x < ?y ] =>
let t := (reify_tower x) in
replace x with t by reflexivity
end.
Definition contender_3 := tower_of_power 10000.
Lemma fund_lemma : forall n m, n < m -> tower_of_power n < tower_of_power m.
Proof.
intros.
induction H.
- simpl.
apply Nat.pow_gt_lin_r; lia.
- simpl.
assert (42 ^ tower_of_power n < 42 ^ tower_of_power m) by (apply Nat.pow_lt_mono_r; lia).
eapply Nat.lt_trans; [exact IHle|].
apply Nat.pow_gt_lin_r; lia.
Qed.
Theorem contender_2_lt_contender_3 : contender_2 < contender_3.
Proof.
unfold contender_2.
Time reify_goal.
unfold contender_3.
apply fund_lemma.
compute; lia.
Qed.
Fixpoint iter (f : nat -> nat) (b : nat) :=
match b with
| 0 => 1
| S b' => f (iter f b')
end.
Fixpoint ack (n a b : nat) :=
match n with
| 0 => S b
| 1 => a + b
| S n' => iter (ack n' a) b
end.
(* This is the current contender for largest number *)
(* Submitted by codyroux *)
Definition contender_4 := ack 5 42 10002.
Lemma ack_0 : forall a b, ack 0 a b = S b.
Proof.
intros; reflexivity.
Qed.
Lemma ack_1 : forall a b, ack 1 a b = a + b.
Proof.
intros; simpl.
reflexivity.
Qed.
Lemma ack_2 : forall a b, ack 2 a b = a * b + 1.
Proof.
intros a b. revert a; induction b; intros; simpl.
- lia.
- simpl in IHb.
rewrite IHb.
lia.
Qed.
Lemma ack_3_aux : forall b a, a ^ b = iter (fun k => a * k) b.
Proof.
induction b; intros; simpl.
- reflexivity.
- rewrite <- IHb.
auto.
Qed.
Definition ge_fun (f g : nat -> nat) :=
forall n, f n <= g n.
Definition mon (f : nat -> nat) := forall n m, n <= m -> f n <= f m.
Definition geS (f : nat -> nat) := forall n, S n <= f n.
Lemma iter_ge_fun : forall f g b,
ge_fun f g -> mon f -> iter f b <= iter g b.
Proof.
intros; induction b; simpl; auto.
transitivity (f (iter g b)); auto.
Qed.
Lemma ack_3 : forall a b, a ^ b <= ack 3 a b.
Proof.
intros; rewrite ack_3_aux.
apply iter_ge_fun.
- intro n.
induction n; try lia.
simpl.
replace (a * S n) with (a + (a * n)) by ring.
lia.
- intros n m; nia.
Qed.
Lemma unfold_iter : forall f b, iter f (S b) = f (iter f b).
Proof. reflexivity. Qed.
Lemma unfold_ack : forall n a b,
2 <= n ->
ack (S n) a b = iter (ack n a) b.
Proof.
intros.
case n as [|n]; [lia|].
case n as [|n]; [lia|].
reflexivity.
Qed.
Lemma ack_4_aux : forall b, tower_of_power b =
iter (fun k => 42 ^ k) (S b).
Proof.
induction b.
- reflexivity.
- simpl.
rewrite IHb.
simpl.
reflexivity.
Qed.
Lemma ack_4 : forall b, tower_of_power b <= ack 4 42 (S b).
Proof.
intros.
rewrite ack_4_aux.
rewrite unfold_ack; [|lia].
apply iter_ge_fun.
- intro n.
apply ack_3.
- intros n m le.
induction le; auto.
replace (42 ^ (S m)) with (42 * (42 ^ m)) by reflexivity.
nia.
Qed.
Lemma mon_ge_iter : forall f,
mon f ->
geS f ->
f 0 <= 1 ->
forall b, f b <= iter f b.
Proof.
intros f mon_f ge_f.
induction b; intros; simpl; [now auto|].
apply mon_f.
transitivity (f b); [apply ge_f | auto].
Qed.
Lemma mon_iter : forall f,
mon f ->
geS f ->
f 0 <= 1 ->
mon (iter f).
Proof.
intros f mon_f geS_f f_0.
intros n m le.
induction le; [now auto|].
simpl.
transitivity (S (iter f m)); now auto.
Qed.
Lemma geS_ack : forall n a, 2 <= a -> geS (ack n a).
Proof.
induction n; intros.
- intro; simpl; lia.
- intro b.
case n as [|n]; [simpl; lia|].
induction b; [simpl; now auto|].
case n as [|n].
+ rewrite ack_2.
nia.
+
rewrite unfold_ack; [|lia].
rewrite unfold_iter.
transitivity (S (ack (3 + n) a b)).
-- apply le_n_S.
apply IHb.
-- apply IHn.
auto.
Qed.
Lemma mon_ack_in_b : forall n a,
2 <= a ->
mon (fun b => ack n a b).
Proof.
induction n; intros.
- simpl; intros b m; lia.
- simpl.
intros b m le.
case n as [|n]; [lia|].
induction le; auto.
rewrite unfold_iter.
transitivity (S (iter (ack (S n) a) m)).
+ lia.
+ apply geS_ack; auto.
Qed.
Theorem contender_3_lt_contender_4 : contender_3 < contender_4.
Proof.
unfold contender_3, contender_4, "<".
rewrite unfold_ack; [|lia].
replace (10002) with (S (S (10000))) by reflexivity.
rewrite unfold_iter.
transitivity (S (iter (ack 4 42)
(S (Init.Nat.of_uint
(Decimal.D1
(Decimal.D0
(Decimal.D0 (Decimal.D0 (Decimal.D0 Decimal.Nil))))))))).
- apply le_n_S.
rewrite unfold_iter.
transitivity (ack 4 42 (S ((Init.Nat.of_uint
(Decimal.D1
(Decimal.D0
(Decimal.D0 (Decimal.D0 (Decimal.D0 Decimal.Nil))))))))).
+
exact (ack_4 10000).
+ apply mon_ack_in_b; [lia|].
assert (geS (iter (ack 4 42))).
-- apply (geS_ack 5 42); lia.
-- apply H.
- apply (geS_ack 4 42); lia.
Qed.