OAI/Geometry/CubicTorus/Profiles/ValueEnclosures72To288.lean

GitHub source file

435 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b71 line 18
2. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e72 line 21
3. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b72 line 22
4. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e73 line 25
5. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b73 line 26
6. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e74 line 29
7. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b74 line 30
8. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e75 line 33
9. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b75 line 34
10. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e76 line 43
11. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b76 line 44
12. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e77 line 47
13. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b77 line 48
14. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e78 line 51
15. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b78 line 52
16. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e79 line 55
17. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b79 line 56
18. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e80 line 59
19. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b80 line 60
20. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e81 line 63
21. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b81 line 64
22. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e82 line 67
23. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b82 line 68
24. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e83 line 71
25. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b83 line 72
26. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e84 line 75
27. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b84 line 76
28. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e85 line 79
29. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b85 line 80
30. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e86 line 83
31. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b86 line 84
32. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e87 line 87
33. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b87 line 88
34. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e88 line 91
35. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b88 line 92
36. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e89 line 95
37. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b89 line 96
38. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e90 line 99
39. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b90 line 100
40. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e91 line 103
41. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b91 line 104
42. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e92 line 107
43. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b92 line 108
44. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e93 line 111
45. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b93 line 112
46. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e94 line 115
47. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b94 line 116
48. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e95 line 119
49. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b95 line 120
50. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e96 line 123
51. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b96 line 124
52. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e97 line 127
53. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b97 line 128
54. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e98 line 131
55. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b98 line 132
56. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e99 line 135
57. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b99 line 136
58. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e100 line 139
59. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b100 line 140
60. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e101 line 143
61. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b101 line 144
62. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e102 line 147
63. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b102 line 148
64. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e103 line 151
65. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b103 line 152
66. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e104 line 155
67. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b104 line 156
68. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e105 line 159
69. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b105 line 160
70. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e106 line 163
71. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b106 line 164
72. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e107 line 167
73. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b107 line 168
74. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e108 line 171
75. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b108 line 172
76. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e109 line 175
77. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b109 line 176
78. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e110 line 179
79. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b110 line 180
80. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e111 line 183
81. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b111 line 184
82. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e112 line 187
83. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b112 line 188
84. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e113 line 191
85. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b113 line 192
86. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e114 line 195
87. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b114 line 196
88. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e115 line 199
89. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b115 line 200
90. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e116 line 203
91. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b116 line 204
92. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e117 line 207
93. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b117 line 208
94. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e118 line 211
95. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b118 line 212
96. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e119 line 215
97. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b119 line 216
98. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e120 line 219
99. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b120 line 220
100. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e121 line 223
101. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b121 line 224
102. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e122 line 227
103. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b122 line 228
104. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e123 line 231
105. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b123 line 232
106. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e124 line 235
107. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b124 line 236
108. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e125 line 239
109. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b125 line 240
110. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e126 line 243
111. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b126 line 244
112. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e127 line 247
113. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b127 line 248
114. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e128 line 251
115. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b128 line 252
116. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e129 line 255
117. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b129 line 256
118. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e130 line 259
119. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b130 line 260
120. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e131 line 263
121. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b131 line 264
122. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e132 line 267
123. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b132 line 268
124. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e133 line 271
125. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b133 line 272
126. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e134 line 281
127. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b134 line 282
128. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e135 line 285
129. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b135 line 286
130. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e136 line 289
131. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b136 line 290
132. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e137 line 293
133. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b137 line 294
134. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e138 line 297
135. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b138 line 298
136. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e139 line 301
137. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b139 line 302
138. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e140 line 305
139. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b140 line 306
140. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e141 line 309
141. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b141 line 310
142. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e142 line 313
143. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b142 line 314
144. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e143 line 317
145. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b143 line 318
146. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e144 line 321
147. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b144 line 322
148. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e145 line 325
149. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b145 line 326
150. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e146 line 329
151. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b146 line 330
152. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e147 line 333
153. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b147 line 334
154. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e148 line 337
155. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b148 line 338
156. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e149 line 341
157. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b149 line 342
158. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e150 line 345
159. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b150 line 346
160. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e151 line 349
161. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b151 line 350
162. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e152 line 353
163. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b152 line 354
164. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e153 line 357
165. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b153 line 358
166. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e154 line 361
167. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b154 line 362
168. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e155 line 365
169. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b155 line 366
170. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e156 line 369
171. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b156 line 370
172. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e157 line 373
173. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b157 line 374
174. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e158 line 377
175. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b158 line 378
176. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e159 line 381
177. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b159 line 382
178. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e160 line 385
179. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b160 line 386
180. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e161 line 389
181. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b161 line 390
182. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e162 line 393
183. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b162 line 394
184. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e163 line 397
185. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b163 line 398
186. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e164 line 401
187. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b164 line 402
188. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e165 line 405
189. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b165 line 406
190. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e166 line 409
191. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b166 line 410
192. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e167 line 413
193. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b167 line 414
194. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e168 line 417
195. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b168 line 418
196. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e169 line 421
197. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b169 line 422
198. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e170 line 425
199. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b170 line 426
200. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e171 line 429
201. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b171 line 430
202. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e172 line 433
203. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b172 line 434
204. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e173 line 437
205. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b173 line 438
206. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e174 line 441
207. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b174 line 442
208. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e175 line 445
209. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b175 line 446
210. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e176 line 449
211. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b176 line 450
212. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e177 line 459
213. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b177 line 460
214. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e178 line 463
215. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b178 line 464
216. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e179 line 467
217. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b179 line 468
218. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e180 line 471
219. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b180 line 472
220. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e181 line 475
221. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b181 line 476
222. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e182 line 479
223. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b182 line 480
224. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e183 line 483
225. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b183 line 484
226. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e184 line 487
227. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b184 line 488
228. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e185 line 491
229. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b185 line 492
230. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e186 line 495
231. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b186 line 496
232. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e187 line 499
233. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b187 line 500
234. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e188 line 503
235. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b188 line 504
236. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e189 line 507
237. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b189 line 508
238. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e190 line 511
239. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b190 line 512
240. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e191 line 515
241. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b191 line 516
242. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e192 line 519
243. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b192 line 520
244. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e193 line 523
245. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b193 line 524
246. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e194 line 527
247. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b194 line 528
248. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e195 line 531
249. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b195 line 532
250. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e196 line 535
251. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b196 line 536
252. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e197 line 539
253. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b197 line 540
254. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e198 line 543
255. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b198 line 544
256. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e199 line 547
257. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b199 line 548
258. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e200 line 551
259. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b200 line 552
260. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e201 line 555
261. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b201 line 556
262. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e202 line 559
263. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b202 line 560
264. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e203 line 563
265. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b203 line 564
266. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e204 line 567
267. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b204 line 568
268. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e205 line 571
269. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b205 line 572
270. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e206 line 575
271. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b206 line 576
272. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e207 line 579
273. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b207 line 580
274. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e208 line 583
275. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b208 line 584
276. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e209 line 587
277. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b209 line 588
278. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e210 line 591
279. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b210 line 592
280. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e211 line 595
281. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b211 line 596
282. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e212 line 599
283. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b212 line 600
284. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e213 line 603
285. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b213 line 604
286. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e214 line 607
287. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b214 line 608
288. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e215 line 611
289. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b215 line 612
290. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e216 line 615
291. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b216 line 616
292. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e217 line 619
293. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b217 line 620
294. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e218 line 623
295. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b218 line 624
296. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e219 line 627
297. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b219 line 628
298. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e220 line 631
299. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b220 line 632
300. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e221 line 635
301. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b221 line 636
302. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e222 line 639
303. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b222 line 640
304. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e223 line 643
305. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b223 line 644
306. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e224 line 647
307. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b224 line 648
308. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e225 line 651
309. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b225 line 652
310. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e226 line 655
311. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b226 line 656
312. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e227 line 659
313. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b227 line 660
314. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e228 line 663
315. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b228 line 664
316. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e229 line 667
317. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b229 line 668
318. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e230 line 671
319. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b230 line 672
320. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e231 line 675
321. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b231 line 676
322. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e232 line 679
323. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b232 line 680
324. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e233 line 689
325. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b233 line 690
326. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e234 line 693
327. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b234 line 694
328. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e235 line 697
329. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b235 line 698
330. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e236 line 701
331. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b236 line 702
332. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e237 line 705
333. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b237 line 706
334. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e238 line 709
335. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b238 line 710
336. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e239 line 713
337. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b239 line 714
338. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e240 line 717
339. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b240 line 718
340. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e241 line 721
341. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b241 line 722
342. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e242 line 725
343. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b242 line 726
344. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e243 line 729
345. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b243 line 730
346. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e244 line 733
347. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b244 line 734
348. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e245 line 737
349. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b245 line 738
350. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e246 line 741
351. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b246 line 742
352. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e247 line 745
353. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b247 line 746
354. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e248 line 755
355. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b248 line 756
356. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e249 line 759
357. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b249 line 760
358. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e250 line 763
359. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b250 line 764
360. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e251 line 767
361. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b251 line 768
362. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e252 line 771
363. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b252 line 772
364. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e253 line 775
365. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b253 line 776
366. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e254 line 779
367. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b254 line 780
368. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e255 line 783
369. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b255 line 784
370. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e256 line 787
371. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b256 line 788
372. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e257 line 791
373. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b257 line 792
374. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e258 line 795
375. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b258 line 796
376. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e259 line 799
377. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b259 line 800
378. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e260 line 803
379. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b260 line 804
380. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e261 line 807
381. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b261 line 808
382. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e262 line 811
383. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b262 line 812
384. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e263 line 815
385. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b263 line 816
386. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e264 line 819
387. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b264 line 820
388. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e265 line 823
389. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b265 line 824
390. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e266 line 827
391. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b266 line 828
392. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e267 line 831
393. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b267 line 832
394. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e268 line 835
395. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b268 line 836
396. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e269 line 839
397. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b269 line 840
398. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e270 line 843
399. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b270 line 844
400. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e271 line 847
401. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b271 line 848
402. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e272 line 851
403. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b272 line 852
404. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e273 line 855
405. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b273 line 856
406. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e274 line 859
407. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b274 line 860
408. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e275 line 863
409. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b275 line 864
410. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e276 line 867
411. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b276 line 868
412. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e277 line 871
413. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b277 line 872
414. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e278 line 875
415. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b278 line 876
416. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e279 line 879
417. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b279 line 880
418. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e280 line 883
419. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b280 line 884
420. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e281 line 887
421. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b281 line 888
422. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e282 line 891
423. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b282 line 892
424. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e283 line 895
425. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b283 line 896
426. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e284 line 899
427. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b284 line 900
428. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e285 line 903
429. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b285 line 904
430. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e286 line 907
431. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b286 line 908
432. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e287 line 911
433. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b287 line 912
434. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e288 line 915
435. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b288 line 916