OAI/Geometry/CubicTorus/Profiles/ValueEnclosures2480To2700.lean

GitHub source file

441 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2480 line 19
2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2480 line 20
3. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2481 line 23
4. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2481 line 24
5. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2482 line 27
6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2482 line 28
7. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2483 line 31
8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2483 line 32
9. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2484 line 35
10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2484 line 36
11. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2485 line 39
12. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2485 line 40
13. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2486 line 43
14. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2486 line 44
15. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2487 line 47
16. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2487 line 48
17. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2488 line 51
18. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2488 line 52
19. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2489 line 55
20. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2489 line 56
21. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2490 line 59
22. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2490 line 60
23. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2491 line 63
24. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2491 line 64
25. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2492 line 67
26. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2492 line 68
27. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2493 line 71
28. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2493 line 72
29. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2494 line 75
30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2494 line 76
31. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2495 line 79
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2495 line 80
33. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2496 line 83
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2496 line 84
35. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2497 line 87
36. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2497 line 88
37. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2498 line 91
38. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2498 line 92
39. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2499 line 95
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2499 line 96
41. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2500 line 99
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2500 line 100
43. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2501 line 103
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2501 line 104
45. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2502 line 107
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2502 line 108
47. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2503 line 111
48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2503 line 112
49. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2504 line 115
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2504 line 116
51. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2505 line 119
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2505 line 120
53. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2506 line 123
54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2506 line 124
55. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2507 line 127
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2507 line 128
57. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2508 line 131
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2508 line 132
59. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2509 line 135
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2509 line 136
61. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2510 line 139
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2510 line 140
63. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2511 line 143
64. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2511 line 144
65. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2512 line 147
66. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2512 line 148
67. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2513 line 151
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2513 line 152
69. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2514 line 155
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2514 line 156
71. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2515 line 159
72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2515 line 160
73. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2516 line 163
74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2516 line 164
75. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2517 line 167
76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2517 line 168
77. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2518 line 171
78. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2518 line 172
79. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2519 line 175
80. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2519 line 176
81. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2520 line 179
82. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2520 line 180
83. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2521 line 183
84. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2521 line 184
85. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2522 line 187
86. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2522 line 188
87. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2523 line 191
88. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2523 line 192
89. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2524 line 195
90. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2524 line 196
91. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2525 line 205
92. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2525 line 206
93. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2526 line 209
94. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2526 line 210
95. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2527 line 213
96. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2527 line 214
97. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2528 line 217
98. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2528 line 218
99. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2529 line 221
100. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2529 line 222
101. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2530 line 225
102. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2530 line 226
103. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2531 line 229
104. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2531 line 230
105. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2532 line 233
106. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2532 line 234
107. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2533 line 237
108. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2533 line 238
109. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2534 line 241
110. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2534 line 242
111. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2535 line 245
112. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2535 line 246
113. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2536 line 249
114. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2536 line 250
115. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2537 line 253
116. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2537 line 254
117. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2538 line 257
118. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2538 line 258
119. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2539 line 261
120. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2539 line 262
121. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2540 line 265
122. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2540 line 266
123. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2541 line 269
124. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2541 line 270
125. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2542 line 273
126. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2542 line 274
127. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2543 line 277
128. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2543 line 278
129. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2544 line 281
130. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2544 line 282
131. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2545 line 285
132. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2545 line 286
133. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2546 line 289
134. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2546 line 290
135. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2547 line 293
136. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2547 line 294
137. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2548 line 297
138. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2548 line 298
139. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2549 line 301
140. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2549 line 302
141. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2550 line 305
142. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2550 line 306
143. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2551 line 309
144. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2551 line 310
145. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2552 line 313
146. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2552 line 314
147. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2553 line 317
148. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2553 line 318
149. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2554 line 321
150. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2554 line 322
151. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2555 line 325
152. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2555 line 326
153. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2556 line 329
154. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2556 line 330
155. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2557 line 333
156. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2557 line 334
157. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2558 line 337
158. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2558 line 338
159. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2559 line 341
160. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2559 line 342
161. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2560 line 345
162. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2560 line 346
163. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2561 line 349
164. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2561 line 350
165. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2562 line 353
166. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2562 line 354
167. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2563 line 357
168. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2563 line 358
169. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2564 line 361
170. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2564 line 362
171. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2565 line 365
172. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2565 line 366
173. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2566 line 369
174. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2566 line 370
175. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2567 line 373
176. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2567 line 374
177. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2568 line 377
178. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2568 line 378
179. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2569 line 381
180. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2569 line 382
181. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2570 line 385
182. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2570 line 386
183. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2571 line 389
184. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2571 line 390
185. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2572 line 393
186. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2572 line 394
187. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2573 line 397
188. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2573 line 398
189. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2574 line 401
190. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2574 line 402
191. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2575 line 405
192. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2575 line 406
193. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2576 line 409
194. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2576 line 410
195. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2577 line 413
196. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2577 line 414
197. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2578 line 417
198. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2578 line 418
199. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2579 line 421
200. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2579 line 422
201. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2580 line 425
202. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2580 line 426
203. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2581 line 429
204. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2581 line 430
205. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2582 line 433
206. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2582 line 434
207. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2583 line 437
208. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2583 line 438
209. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2584 line 441
210. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2584 line 442
211. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2585 line 445
212. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2585 line 446
213. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2586 line 449
214. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2586 line 450
215. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2587 line 453
216. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2587 line 454
217. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2588 line 457
218. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2588 line 458
219. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2589 line 461
220. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2589 line 462
221. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2590 line 465
222. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2590 line 466
223. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2591 line 469
224. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2591 line 470
225. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2592 line 473
226. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2592 line 474
227. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2593 line 477
228. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2593 line 478
229. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2594 line 481
230. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2594 line 482
231. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2595 line 485
232. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2595 line 486
233. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2596 line 489
234. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2596 line 490
235. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2597 line 493
236. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2597 line 494
237. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2598 line 497
238. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2598 line 498
239. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2599 line 501
240. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2599 line 502
241. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2600 line 505
242. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2600 line 506
243. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2601 line 509
244. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2601 line 510
245. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2602 line 513
246. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2602 line 514
247. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2603 line 517
248. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2603 line 518
249. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2604 line 521
250. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2604 line 522
251. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2605 line 525
252. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2605 line 526
253. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2606 line 529
254. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2606 line 530
255. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2607 line 533
256. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2607 line 534
257. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2608 line 537
258. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2608 line 538
259. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2609 line 541
260. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2609 line 542
261. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2610 line 545
262. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2610 line 546
263. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2611 line 549
264. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2611 line 550
265. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2612 line 553
266. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2612 line 554
267. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2613 line 557
268. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2613 line 558
269. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2614 line 561
270. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2614 line 562
271. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2615 line 565
272. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2615 line 566
273. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2616 line 569
274. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2616 line 570
275. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2617 line 573
276. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2617 line 574
277. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2618 line 577
278. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2618 line 578
279. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2619 line 581
280. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2619 line 582
281. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2620 line 585
282. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2620 line 586
283. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2621 line 589
284. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2621 line 590
285. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2622 line 593
286. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2622 line 594
287. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2623 line 597
288. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2623 line 598
289. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2624 line 601
290. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2624 line 602
291. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2625 line 605
292. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2625 line 606
293. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2626 line 609
294. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2626 line 610
295. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2627 line 613
296. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2627 line 614
297. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2628 line 617
298. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2628 line 618
299. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2629 line 621
300. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2629 line 622
301. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2630 line 625
302. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2630 line 626
303. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2631 line 629
304. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2631 line 630
305. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2632 line 633
306. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2632 line 634
307. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2633 line 637
308. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2633 line 638
309. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2634 line 641
310. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2634 line 642
311. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2635 line 645
312. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2635 line 646
313. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2636 line 655
314. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2636 line 656
315. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2637 line 659
316. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2637 line 660
317. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2638 line 663
318. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2638 line 664
319. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2639 line 667
320. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2639 line 668
321. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2640 line 671
322. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2640 line 672
323. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2641 line 675
324. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2641 line 676
325. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2642 line 679
326. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2642 line 680
327. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2643 line 683
328. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2643 line 684
329. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2644 line 687
330. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2644 line 688
331. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2645 line 691
332. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2645 line 692
333. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2646 line 695
334. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2646 line 696
335. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2647 line 699
336. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2647 line 700
337. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2648 line 703
338. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2648 line 704
339. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2649 line 707
340. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2649 line 708
341. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2650 line 711
342. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2650 line 712
343. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2651 line 721
344. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2651 line 722
345. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2652 line 725
346. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2652 line 726
347. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2653 line 729
348. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2653 line 730
349. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2654 line 733
350. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2654 line 734
351. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2655 line 737
352. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2655 line 738
353. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2656 line 741
354. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2656 line 742
355. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2657 line 745
356. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2657 line 746
357. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2658 line 749
358. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2658 line 750
359. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2659 line 753
360. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2659 line 754
361. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2660 line 757
362. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2660 line 758
363. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2661 line 761
364. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2661 line 762
365. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2662 line 765
366. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2662 line 766
367. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2663 line 769
368. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2663 line 770
369. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2664 line 773
370. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2664 line 774
371. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2665 line 777
372. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2665 line 778
373. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2666 line 781
374. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2666 line 782
375. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2667 line 785
376. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2667 line 786
377. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2668 line 789
378. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2668 line 790
379. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2669 line 793
380. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2669 line 794
381. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2670 line 797
382. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2670 line 798
383. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2671 line 801
384. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2671 line 802
385. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2672 line 805
386. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2672 line 806
387. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2673 line 809
388. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2673 line 810
389. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2674 line 813
390. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2674 line 814
391. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2675 line 817
392. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2675 line 818
393. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2676 line 821
394. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2676 line 822
395. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2677 line 825
396. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2677 line 826
397. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2678 line 829
398. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2678 line 830
399. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2679 line 833
400. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2679 line 834
401. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2680 line 837
402. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2680 line 838
403. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2681 line 841
404. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2681 line 842
405. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2682 line 845
406. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2682 line 846
407. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2683 line 849
408. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2683 line 850
409. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2684 line 853
410. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2684 line 854
411. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2685 line 857
412. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2685 line 858
413. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2686 line 861
414. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2686 line 862
415. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2687 line 865
416. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2687 line 866
417. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2688 line 869
418. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2688 line 870
419. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2689 line 873
420. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2689 line 874
421. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2690 line 877
422. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2690 line 878
423. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2691 line 881
424. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2691 line 882
425. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2692 line 885
426. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2692 line 886
427. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2693 line 889
428. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2693 line 890
429. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2694 line 893
430. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2694 line 894
431. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2695 line 897
432. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2695 line 898
433. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2696 line 901
434. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2696 line 902
435. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2697 line 905
436. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2697 line 906
437. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2698 line 909
438. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2698 line 910
439. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2699 line 913
440. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2699 line 914
441. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2700 line 917