OAI/Geometry/CubicTorus/Profiles/ValueEnclosures2263To2479.lean

GitHub source file

435 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2262 line 18
2. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2263 line 21
3. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2263 line 22
4. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2264 line 25
5. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2264 line 26
6. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2265 line 29
7. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2265 line 30
8. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2266 line 33
9. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2266 line 34
10. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2267 line 37
11. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2267 line 38
12. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2268 line 41
13. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2268 line 42
14. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2269 line 45
15. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2269 line 46
16. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2270 line 49
17. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2270 line 50
18. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2271 line 53
19. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2271 line 54
20. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2272 line 57
21. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2272 line 58
22. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2273 line 61
23. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2273 line 62
24. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2274 line 71
25. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2274 line 72
26. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2275 line 75
27. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2275 line 76
28. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2276 line 79
29. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2276 line 80
30. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2277 line 83
31. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2277 line 84
32. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2278 line 87
33. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2278 line 88
34. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2279 line 91
35. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2279 line 92
36. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2280 line 95
37. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2280 line 96
38. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2281 line 99
39. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2281 line 100
40. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2282 line 103
41. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2282 line 104
42. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2283 line 107
43. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2283 line 108
44. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2284 line 111
45. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2284 line 112
46. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2285 line 115
47. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2285 line 116
48. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2286 line 119
49. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2286 line 120
50. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2287 line 123
51. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2287 line 124
52. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2288 line 127
53. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2288 line 128
54. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2289 line 137
55. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2289 line 138
56. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2290 line 141
57. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2290 line 142
58. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2291 line 145
59. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2291 line 146
60. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2292 line 149
61. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2292 line 150
62. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2293 line 153
63. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2293 line 154
64. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2294 line 157
65. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2294 line 158
66. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2295 line 161
67. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2295 line 162
68. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2296 line 165
69. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2296 line 166
70. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2297 line 169
71. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2297 line 170
72. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2298 line 173
73. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2298 line 174
74. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2299 line 177
75. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2299 line 178
76. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2300 line 181
77. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2300 line 182
78. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2301 line 185
79. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2301 line 186
80. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2302 line 189
81. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2302 line 190
82. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2303 line 193
83. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2303 line 194
84. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2304 line 197
85. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2304 line 198
86. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2305 line 201
87. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2305 line 202
88. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2306 line 205
89. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2306 line 206
90. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2307 line 209
91. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2307 line 210
92. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2308 line 213
93. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2308 line 214
94. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2309 line 217
95. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2309 line 218
96. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2310 line 221
97. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2310 line 222
98. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2311 line 225
99. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2311 line 226
100. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2312 line 229
101. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2312 line 230
102. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2313 line 233
103. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2313 line 234
104. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2314 line 237
105. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2314 line 238
106. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2315 line 241
107. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2315 line 242
108. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2316 line 245
109. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2316 line 246
110. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2317 line 249
111. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2317 line 250
112. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2318 line 253
113. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2318 line 254
114. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2319 line 257
115. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2319 line 258
116. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2320 line 261
117. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2320 line 262
118. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2321 line 265
119. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2321 line 266
120. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2322 line 269
121. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2322 line 270
122. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2323 line 273
123. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2323 line 274
124. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2324 line 277
125. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2324 line 278
126. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2325 line 281
127. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2325 line 282
128. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2326 line 285
129. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2326 line 286
130. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2327 line 289
131. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2327 line 290
132. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2328 line 293
133. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2328 line 294
134. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2329 line 297
135. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2329 line 298
136. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2330 line 301
137. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2330 line 302
138. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2331 line 305
139. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2331 line 306
140. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2332 line 309
141. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2332 line 310
142. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2333 line 313
143. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2333 line 314
144. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2334 line 317
145. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2334 line 318
146. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2335 line 321
147. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2335 line 322
148. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2336 line 325
149. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2336 line 326
150. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2337 line 329
151. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2337 line 330
152. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2338 line 333
153. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2338 line 334
154. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2339 line 337
155. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2339 line 338
156. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2340 line 341
157. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2340 line 342
158. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2341 line 345
159. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2341 line 346
160. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2342 line 349
161. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2342 line 350
162. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2343 line 353
163. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2343 line 354
164. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2344 line 363
165. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2344 line 364
166. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2345 line 367
167. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2345 line 368
168. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2346 line 371
169. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2346 line 372
170. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2347 line 375
171. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2347 line 376
172. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2348 line 379
173. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2348 line 380
174. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2349 line 383
175. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2349 line 384
176. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2350 line 387
177. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2350 line 388
178. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2351 line 391
179. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2351 line 392
180. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2352 line 395
181. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2352 line 396
182. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2353 line 399
183. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2353 line 400
184. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2354 line 403
185. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2354 line 404
186. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2355 line 407
187. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2355 line 408
188. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2356 line 411
189. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2356 line 412
190. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2357 line 415
191. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2357 line 416
192. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2358 line 419
193. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2358 line 420
194. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2359 line 423
195. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2359 line 424
196. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2360 line 427
197. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2360 line 428
198. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2361 line 431
199. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2361 line 432
200. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2362 line 435
201. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2362 line 436
202. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2363 line 439
203. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2363 line 440
204. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2364 line 443
205. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2364 line 444
206. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2365 line 447
207. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2365 line 448
208. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2366 line 451
209. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2366 line 452
210. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2367 line 455
211. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2367 line 456
212. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2368 line 459
213. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2368 line 460
214. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2369 line 463
215. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2369 line 464
216. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2370 line 467
217. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2370 line 468
218. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2371 line 471
219. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2371 line 472
220. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2372 line 475
221. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2372 line 476
222. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2373 line 479
223. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2373 line 480
224. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2374 line 483
225. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2374 line 484
226. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2375 line 487
227. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2375 line 488
228. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2376 line 491
229. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2376 line 492
230. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2377 line 495
231. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2377 line 496
232. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2378 line 499
233. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2378 line 500
234. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2379 line 503
235. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2379 line 504
236. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2380 line 507
237. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2380 line 508
238. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2381 line 511
239. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2381 line 512
240. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2382 line 515
241. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2382 line 516
242. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2383 line 519
243. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2383 line 520
244. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2384 line 523
245. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2384 line 524
246. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2385 line 527
247. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2385 line 528
248. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2386 line 531
249. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2386 line 532
250. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2387 line 535
251. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2387 line 536
252. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2388 line 539
253. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2388 line 540
254. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2389 line 543
255. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2389 line 544
256. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2390 line 547
257. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2390 line 548
258. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2391 line 551
259. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2391 line 552
260. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2392 line 555
261. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2392 line 556
262. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2393 line 559
263. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2393 line 560
264. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2394 line 563
265. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2394 line 564
266. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2395 line 567
267. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2395 line 568
268. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2396 line 571
269. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2396 line 572
270. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2397 line 575
271. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2397 line 576
272. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2398 line 579
273. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2398 line 580
274. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2399 line 583
275. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2399 line 584
276. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2400 line 587
277. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2400 line 588
278. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2401 line 591
279. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2401 line 592
280. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2402 line 595
281. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2402 line 596
282. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2403 line 599
283. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2403 line 600
284. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2404 line 603
285. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2404 line 604
286. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2405 line 607
287. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2405 line 608
288. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2406 line 611
289. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2406 line 612
290. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2407 line 615
291. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2407 line 616
292. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2408 line 619
293. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2408 line 620
294. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2409 line 623
295. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2409 line 624
296. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2410 line 627
297. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2410 line 628
298. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2411 line 631
299. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2411 line 632
300. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2412 line 635
301. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2412 line 636
302. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2413 line 639
303. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2413 line 640
304. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2414 line 643
305. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2414 line 644
306. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2415 line 647
307. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2415 line 648
308. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2416 line 651
309. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2416 line 652
310. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2417 line 655
311. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2417 line 656
312. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2418 line 659
313. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2418 line 660
314. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2419 line 663
315. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2419 line 664
316. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2420 line 667
317. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2420 line 668
318. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2421 line 671
319. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2421 line 672
320. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2422 line 675
321. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2422 line 676
322. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2423 line 679
323. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2423 line 680
324. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2424 line 683
325. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2424 line 684
326. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2425 line 687
327. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2425 line 688
328. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2426 line 691
329. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2426 line 692
330. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2427 line 695
331. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2427 line 696
332. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2428 line 699
333. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2428 line 700
334. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2429 line 703
335. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2429 line 704
336. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2430 line 707
337. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2430 line 708
338. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2431 line 711
339. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2431 line 712
340. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2432 line 715
341. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2432 line 716
342. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2433 line 719
343. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2433 line 720
344. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2434 line 723
345. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2434 line 724
346. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2435 line 727
347. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2435 line 728
348. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2436 line 731
349. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2436 line 732
350. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2437 line 735
351. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2437 line 736
352. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2438 line 739
353. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2438 line 740
354. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2439 line 743
355. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2439 line 744
356. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2440 line 747
357. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2440 line 748
358. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2441 line 751
359. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2441 line 752
360. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2442 line 755
361. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2442 line 756
362. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2443 line 759
363. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2443 line 760
364. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2444 line 763
365. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2444 line 764
366. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2445 line 767
367. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2445 line 768
368. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2446 line 771
369. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2446 line 772
370. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2447 line 775
371. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2447 line 776
372. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2448 line 779
373. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2448 line 780
374. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2449 line 783
375. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2449 line 784
376. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2450 line 787
377. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2450 line 788
378. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2451 line 791
379. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2451 line 792
380. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2452 line 795
381. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2452 line 796
382. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2453 line 799
383. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2453 line 800
384. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2454 line 803
385. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2454 line 804
386. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2455 line 813
387. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2455 line 814
388. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2456 line 817
389. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2456 line 818
390. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2457 line 821
391. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2457 line 822
392. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2458 line 825
393. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2458 line 826
394. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2459 line 829
395. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2459 line 830
396. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2460 line 833
397. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2460 line 834
398. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2461 line 837
399. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2461 line 838
400. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2462 line 841
401. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2462 line 842
402. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2463 line 845
403. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2463 line 846
404. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2464 line 849
405. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2464 line 850
406. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2465 line 853
407. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2465 line 854
408. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2466 line 857
409. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2466 line 858
410. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2467 line 861
411. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2467 line 862
412. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2468 line 865
413. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2468 line 866
414. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2469 line 869
415. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2469 line 870
416. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2470 line 879
417. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2470 line 880
418. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2471 line 883
419. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2471 line 884
420. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2472 line 887
421. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2472 line 888
422. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2473 line 891
423. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2473 line 892
424. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2474 line 895
425. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2474 line 896
426. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2475 line 899
427. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2475 line 900
428. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2476 line 903
429. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2476 line 904
430. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2477 line 907
431. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2477 line 908
432. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2478 line 911
433. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2478 line 912
434. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2479 line 915
435. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2479 line 916