OAI/Geometry/CubicTorus/Profiles/ValueEnclosures289To507.lean

GitHub source file

438 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e289 line 19
2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b289 line 20
3. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e290 line 23
4. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b290 line 24
5. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e291 line 27
6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b291 line 28
7. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e292 line 31
8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b292 line 32
9. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e293 line 35
10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b293 line 36
11. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e294 line 39
12. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b294 line 40
13. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e295 line 43
14. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b295 line 44
15. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e296 line 47
16. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b296 line 48
17. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e297 line 51
18. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b297 line 52
19. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e298 line 55
20. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b298 line 56
21. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e299 line 59
22. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b299 line 60
23. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e300 line 63
24. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b300 line 64
25. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e301 line 67
26. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b301 line 68
27. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e302 line 71
28. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b302 line 72
29. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e303 line 81
30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b303 line 82
31. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e304 line 85
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b304 line 86
33. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e305 line 89
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b305 line 90
35. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e306 line 93
36. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b306 line 94
37. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e307 line 97
38. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b307 line 98
39. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e308 line 101
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b308 line 102
41. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e309 line 105
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b309 line 106
43. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e310 line 109
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b310 line 110
45. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e311 line 113
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b311 line 114
47. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e312 line 117
48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b312 line 118
49. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e313 line 121
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b313 line 122
51. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e314 line 125
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b314 line 126
53. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e315 line 129
54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b315 line 130
55. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e316 line 133
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b316 line 134
57. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e317 line 137
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b317 line 138
59. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e318 line 141
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b318 line 142
61. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e319 line 145
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b319 line 146
63. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e320 line 149
64. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b320 line 150
65. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e321 line 153
66. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b321 line 154
67. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e322 line 157
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b322 line 158
69. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e323 line 161
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b323 line 162
71. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e324 line 165
72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b324 line 166
73. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e325 line 169
74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b325 line 170
75. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e326 line 173
76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b326 line 174
77. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e327 line 177
78. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b327 line 178
79. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e328 line 181
80. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b328 line 182
81. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e329 line 185
82. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b329 line 186
83. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e330 line 189
84. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b330 line 190
85. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e331 line 193
86. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b331 line 194
87. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e332 line 197
88. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b332 line 198
89. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e333 line 201
90. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b333 line 202
91. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e334 line 205
92. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b334 line 206
93. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e335 line 209
94. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b335 line 210
95. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e336 line 213
96. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b336 line 214
97. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e337 line 217
98. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b337 line 218
99. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e338 line 221
100. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b338 line 222
101. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e339 line 225
102. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b339 line 226
103. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e340 line 229
104. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b340 line 230
105. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e341 line 233
106. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b341 line 234
107. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e342 line 237
108. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b342 line 238
109. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e343 line 241
110. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b343 line 242
111. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e344 line 245
112. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b344 line 246
113. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e345 line 249
114. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b345 line 250
115. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e346 line 253
116. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b346 line 254
117. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e347 line 257
118. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b347 line 258
119. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e348 line 261
120. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b348 line 262
121. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e349 line 265
122. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b349 line 266
123. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e350 line 269
124. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b350 line 270
125. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e351 line 273
126. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b351 line 274
127. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e352 line 277
128. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b352 line 278
129. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e353 line 281
130. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b353 line 282
131. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e354 line 285
132. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b354 line 286
133. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e355 line 289
134. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b355 line 290
135. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e356 line 293
136. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b356 line 294
137. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e357 line 297
138. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b357 line 298
139. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e358 line 301
140. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b358 line 302
141. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e359 line 305
142. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b359 line 306
143. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e360 line 309
144. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b360 line 310
145. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e361 line 313
146. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b361 line 314
147. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e362 line 317
148. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b362 line 318
149. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e363 line 321
150. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b363 line 322
151. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e364 line 325
152. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b364 line 326
153. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e365 line 329
154. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b365 line 330
155. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e366 line 333
156. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b366 line 334
157. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e367 line 337
158. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b367 line 338
159. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e368 line 341
160. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b368 line 342
161. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e369 line 345
162. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b369 line 346
163. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e370 line 349
164. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b370 line 350
165. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e371 line 353
166. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b371 line 354
167. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e372 line 357
168. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b372 line 358
169. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e373 line 361
170. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b373 line 362
171. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e374 line 365
172. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b374 line 366
173. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e375 line 369
174. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b375 line 370
175. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e376 line 373
176. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b376 line 374
177. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e377 line 377
178. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b377 line 378
179. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e378 line 381
180. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b378 line 382
181. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e379 line 385
182. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b379 line 386
183. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e380 line 395
184. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b380 line 396
185. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e381 line 399
186. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b381 line 400
187. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e382 line 403
188. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b382 line 404
189. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e383 line 407
190. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b383 line 408
191. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e384 line 411
192. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b384 line 412
193. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e385 line 415
194. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b385 line 416
195. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e386 line 419
196. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b386 line 420
197. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e387 line 423
198. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b387 line 424
199. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e388 line 427
200. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b388 line 428
201. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e389 line 431
202. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b389 line 432
203. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e390 line 435
204. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b390 line 436
205. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e391 line 439
206. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b391 line 440
207. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e392 line 443
208. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b392 line 444
209. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e393 line 447
210. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b393 line 448
211. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e394 line 451
212. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b394 line 452
213. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e395 line 461
214. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b395 line 462
215. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e396 line 465
216. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b396 line 466
217. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e397 line 469
218. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b397 line 470
219. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e398 line 473
220. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b398 line 474
221. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e399 line 477
222. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b399 line 478
223. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e400 line 481
224. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b400 line 482
225. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e401 line 485
226. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b401 line 486
227. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e402 line 489
228. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b402 line 490
229. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e403 line 493
230. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b403 line 494
231. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e404 line 497
232. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b404 line 498
233. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e405 line 501
234. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b405 line 502
235. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e406 line 505
236. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b406 line 506
237. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e407 line 509
238. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b407 line 510
239. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e408 line 513
240. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b408 line 514
241. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e409 line 517
242. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b409 line 518
243. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e410 line 521
244. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b410 line 522
245. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e411 line 525
246. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b411 line 526
247. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e412 line 529
248. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b412 line 530
249. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e413 line 533
250. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b413 line 534
251. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e414 line 537
252. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b414 line 538
253. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e415 line 541
254. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b415 line 542
255. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e416 line 545
256. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b416 line 546
257. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e417 line 549
258. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b417 line 550
259. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e418 line 553
260. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b418 line 554
261. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e419 line 557
262. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b419 line 558
263. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e420 line 561
264. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b420 line 562
265. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e421 line 565
266. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b421 line 566
267. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e422 line 569
268. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b422 line 570
269. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e423 line 573
270. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b423 line 574
271. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e424 line 577
272. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b424 line 578
273. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e425 line 581
274. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b425 line 582
275. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e426 line 585
276. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b426 line 586
277. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e427 line 589
278. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b427 line 590
279. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e428 line 593
280. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b428 line 594
281. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e429 line 597
282. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b429 line 598
283. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e430 line 601
284. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b430 line 602
285. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e431 line 605
286. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b431 line 606
287. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e432 line 609
288. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b432 line 610
289. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e433 line 613
290. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b433 line 614
291. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e434 line 617
292. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b434 line 618
293. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e435 line 621
294. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b435 line 622
295. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e436 line 625
296. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b436 line 626
297. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e437 line 629
298. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b437 line 630
299. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e438 line 633
300. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b438 line 634
301. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e439 line 637
302. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b439 line 638
303. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e440 line 641
304. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b440 line 642
305. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e441 line 645
306. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b441 line 646
307. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e442 line 649
308. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b442 line 650
309. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e443 line 653
310. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b443 line 654
311. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e444 line 657
312. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b444 line 658
313. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e445 line 661
314. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b445 line 662
315. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e446 line 665
316. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b446 line 666
317. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e447 line 669
318. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b447 line 670
319. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e448 line 673
320. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b448 line 674
321. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e449 line 677
322. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b449 line 678
323. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e450 line 687
324. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b450 line 688
325. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e451 line 691
326. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b451 line 692
327. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e452 line 695
328. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b452 line 696
329. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e453 line 699
330. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b453 line 700
331. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e454 line 703
332. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b454 line 704
333. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e455 line 707
334. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b455 line 708
335. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e456 line 711
336. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b456 line 712
337. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e457 line 715
338. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b457 line 716
339. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e458 line 719
340. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b458 line 720
341. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e459 line 723
342. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b459 line 724
343. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e460 line 727
344. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b460 line 728
345. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e461 line 731
346. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b461 line 732
347. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e462 line 735
348. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b462 line 736
349. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e463 line 739
350. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b463 line 740
351. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e464 line 743
352. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b464 line 744
353. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e465 line 747
354. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b465 line 748
355. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e466 line 751
356. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b466 line 752
357. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e467 line 755
358. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b467 line 756
359. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e468 line 759
360. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b468 line 760
361. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e469 line 763
362. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b469 line 764
363. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e470 line 767
364. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b470 line 768
365. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e471 line 771
366. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b471 line 772
367. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e472 line 775
368. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b472 line 776
369. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e473 line 779
370. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b473 line 780
371. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e474 line 783
372. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b474 line 784
373. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e475 line 787
374. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b475 line 788
375. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e476 line 791
376. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b476 line 792
377. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e477 line 795
378. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b477 line 796
379. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e478 line 799
380. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b478 line 800
381. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e479 line 803
382. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b479 line 804
383. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e480 line 807
384. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b480 line 808
385. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e481 line 811
386. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b481 line 812
387. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e482 line 815
388. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b482 line 816
389. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e483 line 819
390. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b483 line 820
391. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e484 line 823
392. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b484 line 824
393. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e485 line 827
394. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b485 line 828
395. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e486 line 831
396. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b486 line 832
397. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e487 line 835
398. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b487 line 836
399. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e488 line 839
400. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b488 line 840
401. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e489 line 843
402. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b489 line 844
403. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e490 line 847
404. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b490 line 848
405. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e491 line 851
406. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b491 line 852
407. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e492 line 855
408. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b492 line 856
409. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e493 line 859
410. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b493 line 860
411. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e494 line 863
412. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b494 line 864
413. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e495 line 867
414. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b495 line 868
415. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e496 line 871
416. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b496 line 872
417. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e497 line 875
418. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b497 line 876
419. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e498 line 879
420. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b498 line 880
421. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e499 line 883
422. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b499 line 884
423. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e500 line 887
424. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b500 line 888
425. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e501 line 891
426. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b501 line 892
427. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e502 line 895
428. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b502 line 896
429. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e503 line 899
430. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b503 line 900
431. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e504 line 903
432. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b504 line 904
433. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e505 line 907
434. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b505 line 908
435. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e506 line 911
436. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b506 line 912
437. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e507 line 915
438. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b507 line 916