blob: 829f9c28a4fe7ad23e8f59fb5161adf69adc3ace (
plain)
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
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
|
1 succn_inj
2 eqnP
3 eqnE
4 eqSS
5 nat_irrelevance
6 addnE
7 plusE
8 add0n
9 addSn
10 add1n
11 addn0
12 addnS
13 addSnnS
14 addnCA
15 addnC
16 addn1
17 addnA
18 addnAC
19 addnACA
20 addn_eq0
21 eqn_add2l
22 eqn_add2r
23 addnI
24 addIn
25 addn2
26 add2n
27 addn3
28 add3n
29 addn4
30 add4n
31 subnE
32 minusE
33 sub0n
34 subn0
35 subnn
36 subSS
37 subn1
38 subn2
39 subnDl
40 subnDr
41 addKn
42 addnK
43 subSnn
44 subnDA
45 subnAC
46 subnS
47 subSKn
48 ltnS
49 leq0n
50 ltn0Sn
51 ltn0
52 leqnn
53 ltnSn
54 eq_leq
55 leqnSn
56 leq_pred
57 leqSpred
58 ltn_predK
59 prednK
60 leqNgt
61 ltnNge
62 ltnn
63 leqn0
64 lt0n
65 lt0n_neq0
66 eqn0Ngt
67 neq0_lt0n
68 eqn_leq
69 anti_leq
70 neq_ltn
71 gtn_eqF
72 ltn_eqF
73 leq_eqVlt
74 ltn_neqAle
75 leq_trans
76 leq_ltn_trans
77 ltnW
78 leqW
79 ltn_trans
80 leq_total
81 leP
82 le_irrelevance
83 ltP
84 lt_irrelevance
85 leqP
86 ltnP
87 posnP
88 ltngtP
89 leq_add2l
90 ltn_add2l
91 leq_add2r
92 ltn_add2r
93 leq_add
94 leq_addr
95 leq_addl
96 ltn_addr
97 ltn_addl
98 addn_gt0
99 subn_gt0
100 subn_eq0
101 leq_subLR
102 leq_subr
103 subnKC
104 subnK
105 addnBA
106 subnBA
107 subKn
108 subSn
109 subnSK
110 leq_sub2r
111 leq_sub2l
112 leq_sub
113 ltn_sub2r
114 ltn_sub2l
115 ltn_subRL
116 subn_if_gt
117 max0n
118 maxn0
119 maxnC
120 maxnE
121 maxnAC
122 maxnA
123 maxnCA
124 maxnACA
125 maxn_idPl
126 maxn_idPr
127 maxnn
128 leq_max
129 leq_maxl
130 leq_maxr
131 gtn_max
132 geq_max
133 maxnSS
134 addn_maxl
135 addn_maxr
136 min0n
137 minn0
138 minnC
139 addn_min_max
140 minnE
141 minnAC
142 minnA
143 minnCA
144 minnACA
145 minn_idPl
146 minn_idPr
147 minnn
148 leq_min
149 gtn_min
150 geq_min
151 geq_minl
152 geq_minr
153 addn_minr
154 addn_minl
155 minnSS
156 maxnK
157 maxKn
158 minnK
159 minKn
160 maxn_minl
161 maxn_minr
162 minn_maxl
163 minn_maxr
164 find_ex_minn
165 ex_minnP
166 ex_maxn_subproof
167 ex_maxnP
168 eq_ex_minn
169 eq_ex_maxn
170 iterSr
171 iterS
172 iter_add
173 iteriS
174 iteropS
175 eq_iter
176 eq_iteri
177 eq_iterop
178 multE
179 mulnE
180 mul0n
181 muln0
182 mul1n
183 mulSn
184 mulSnr
185 mulnS
186 mulnSr
187 muln1
188 mulnC
189 mulnDl
190 mulnDr
191 mulnBl
192 mulnBr
193 mulnA
194 mulnCA
195 mulnAC
196 mulnACA
197 muln_eq0
198 muln_eq1
199 muln_gt0
200 leq_pmull
201 leq_pmulr
202 leq_mul2l
203 leq_mul2r
204 leq_mul
205 eqn_mul2l
206 eqn_mul2r
207 leq_pmul2l
208 leq_pmul2r
209 eqn_pmul2l
210 eqn_pmul2r
211 ltn_mul2l
212 ltn_mul2r
213 ltn_pmul2l
214 ltn_pmul2r
215 ltn_Pmull
216 ltn_Pmulr
217 ltn_mul
218 maxn_mulr
219 maxn_mull
220 minn_mulr
221 minn_mull
222 expnE
223 expn0
224 expn1
225 expnS
226 expnSr
227 exp0n
228 exp1n
229 expnD
230 expnMn
231 expnM
232 expnAC
233 expn_gt0
234 expn_eq0
235 ltn_expl
236 leq_exp2l
237 ltn_exp2l
238 eqn_exp2l
239 expnI
240 leq_pexp2l
241 ltn_pexp2l
242 ltn_exp2r
243 leq_exp2r
244 eqn_exp2r
245 expIn
246 factE
247 fact0
248 factS
249 fact_gt0
250 leq_b1
251 addn_negb
252 eqb0
253 lt0b
254 sub1b
255 mulnb
256 oddb
257 odd_add
258 odd_sub
259 odd_opp
260 odd_mul
261 odd_exp
262 doubleE
263 double0
264 doubleS
265 addnn
266 mul2n
267 muln2
268 doubleD
269 doubleB
270 leq_double
271 ltn_double
272 ltn_Sdouble
273 leq_Sdouble
274 odd_double
275 double_gt0
276 double_eq0
277 doubleMl
278 doubleMr
279 doubleK
280 uphalf_double
281 uphalf_half
282 odd_double_half
283 half_bit_double
284 halfD
285 half_leq
286 half_gt0
287 mulnn
288 sqrnD
289 sqrn_sub
290 sqrnD_sub
291 subn_sqr
292 ltn_sqr
293 leq_sqr
294 sqrn_gt0
295 eqn_sqr
296 sqrn_inj
297 leqifP
298 leqif_refl
299 leqif_trans
300 monotone_leqif
301 leqif_geq
302 leqif_eq
303 geq_leqif
304 ltn_leqif
305 leqif_add
306 leqif_mul
307 nat_Cauchy
308 nat_AGM2
309 addE
310 doubleE
311 add_mulE
312 mulE
313 mul_expE
314 expE
315 oddE
316 eq_binP
317 bin_of_natK
318 nat_of_binK
319 nat_of_succ_gt0
320 nat_of_addn_gt0
321 nat_of_add_bin
322 nat_of_mul_bin
323 nat_of_exp_bin
324 nat_semi_ring
325 nat_semi_morph
326 nat_power_theory
|
