OAI/Geometry/CubicTorus/Profiles/ValueEnclosures3143To3335.lean

GitHub source file

416 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3143 line 19
2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3143 line 20
3. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3144 line 23
4. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3144 line 24
5. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3145 line 33
6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3145 line 34
7. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3146 line 37
8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3146 line 38
9. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3147 line 41
10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3147 line 42
11. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3148 line 45
12. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3148 line 46
13. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3149 line 49
14. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3149 line 50
15. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3150 line 53
16. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3150 line 54
17. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3151 line 57
18. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3151 line 58
19. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3152 line 61
20. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3152 line 62
21. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3153 line 65
22. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3153 line 66
23. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3154 line 69
24. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3154 line 70
25. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3155 line 73
26. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3155 line 74
27. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3156 line 77
28. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3156 line 78
29. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3157 line 81
30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3157 line 82
31. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3158 line 85
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3158 line 86
33. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3159 line 89
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3159 line 90
35. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3160 line 93
36. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3160 line 94
37. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3161 line 97
38. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3161 line 98
39. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3162 line 101
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3162 line 102
41. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3163 line 105
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3163 line 106
43. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3164 line 109
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3164 line 110
45. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3165 line 113
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3165 line 114
47. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3166 line 117
48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3166 line 118
49. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3167 line 121
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3167 line 122
51. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3168 line 125
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3168 line 126
53. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3169 line 129
54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3169 line 130
55. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3170 line 133
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3170 line 134
57. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3171 line 137
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3171 line 138
59. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3172 line 141
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3172 line 142
61. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3173 line 145
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3173 line 146
63. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3174 line 149
64. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3174 line 150
65. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3175 line 153
66. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3175 line 154
67. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3176 line 157
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3176 line 158
69. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3177 line 161
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3177 line 162
71. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3178 line 165
72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3178 line 166
73. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3179 line 169
74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3179 line 170
75. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3180 line 173
76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3180 line 174
77. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3181 line 177
78. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3181 line 178
79. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3182 line 181
80. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3182 line 182
81. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3183 line 185
82. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3183 line 186
83. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3184 line 189
84. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3184 line 190
85. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3185 line 193
86. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3185 line 194
87. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3186 line 197
88. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3186 line 198
89. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3187 line 201
90. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3187 line 202
91. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3188 line 205
92. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3188 line 206
93. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3189 line 209
94. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3189 line 210
95. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3190 line 213
96. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3190 line 214
97. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3191 line 217
98. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3191 line 218
99. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3192 line 221
100. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3192 line 222
101. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3193 line 225
102. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3193 line 226
103. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3194 line 229
104. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3194 line 230
105. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3195 line 233
106. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3195 line 234
107. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3196 line 237
108. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3196 line 238
109. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3197 line 241
110. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3197 line 242
111. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3198 line 245
112. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3198 line 246
113. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3199 line 249
114. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3199 line 250
115. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3200 line 253
116. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3200 line 254
117. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3201 line 257
118. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3201 line 258
119. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3202 line 261
120. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3202 line 262
121. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3203 line 265
122. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3203 line 266
123. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3204 line 269
124. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3204 line 270
125. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3205 line 273
126. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3205 line 274
127. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3206 line 277
128. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3206 line 278
129. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3207 line 281
130. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3207 line 282
131. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3208 line 285
132. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3208 line 286
133. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3209 line 289
134. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3209 line 290
135. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3210 line 293
136. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3210 line 294
137. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3211 line 297
138. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3211 line 298
139. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3212 line 301
140. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3212 line 302
141. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3213 line 305
142. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3213 line 306
143. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3214 line 309
144. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3214 line 310
145. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3215 line 313
146. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3215 line 314
147. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3216 line 317
148. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3216 line 318
149. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3217 line 321
150. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3217 line 322
151. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3218 line 325
152. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3218 line 326
153. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3219 line 329
154. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3219 line 330
155. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3220 line 333
156. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3220 line 334
157. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3221 line 337
158. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3221 line 338
159. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3222 line 341
160. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3222 line 342
161. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3223 line 345
162. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3223 line 346
163. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3224 line 349
164. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3224 line 350
165. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3225 line 353
166. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3225 line 354
167. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3226 line 357
168. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3226 line 358
169. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3227 line 361
170. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3227 line 362
171. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3228 line 371
172. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3228 line 372
173. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3229 line 375
174. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3229 line 376
175. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3230 line 379
176. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3230 line 380
177. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3231 line 383
178. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3231 line 384
179. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3232 line 387
180. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3232 line 388
181. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3233 line 391
182. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3233 line 392
183. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3234 line 395
184. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3234 line 396
185. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3235 line 399
186. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3235 line 400
187. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3236 line 403
188. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3236 line 404
189. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3237 line 407
190. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3237 line 408
191. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3238 line 411
192. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3238 line 412
193. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3239 line 415
194. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3239 line 416
195. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3240 line 419
196. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3240 line 420
197. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3241 line 423
198. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3241 line 424
199. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3242 line 427
200. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3242 line 428
201. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3243 line 431
202. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3243 line 432
203. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3244 line 435
204. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3244 line 436
205. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3245 line 439
206. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3245 line 440
207. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3246 line 443
208. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3246 line 444
209. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3247 line 447
210. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3247 line 448
211. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3248 line 451
212. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3248 line 452
213. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3249 line 455
214. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3249 line 456
215. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3250 line 459
216. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3250 line 460
217. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3251 line 463
218. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3251 line 464
219. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3252 line 467
220. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3252 line 468
221. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3253 line 471
222. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3253 line 472
223. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3254 line 475
224. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3254 line 476
225. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3255 line 479
226. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3255 line 480
227. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3256 line 483
228. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3256 line 484
229. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3257 line 487
230. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3257 line 488
231. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3258 line 491
232. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3258 line 492
233. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3259 line 495
234. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3259 line 496
235. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3260 line 499
236. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3260 line 500
237. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3261 line 503
238. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3261 line 504
239. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3262 line 507
240. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3262 line 508
241. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3263 line 511
242. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3263 line 512
243. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3264 line 515
244. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3264 line 516
245. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3265 line 519
246. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3265 line 520
247. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3266 line 523
248. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3266 line 524
249. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3267 line 527
250. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3267 line 528
251. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3268 line 531
252. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3268 line 532
253. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3269 line 535
254. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3269 line 536
255. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3270 line 539
256. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3270 line 540
257. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3271 line 543
258. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3271 line 544
259. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3272 line 547
260. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3272 line 548
261. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3273 line 551
262. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3273 line 552
263. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3274 line 555
264. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3274 line 556
265. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3275 line 559
266. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3275 line 560
267. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3276 line 563
268. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3276 line 564
269. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3277 line 573
270. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3277 line 574
271. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3278 line 577
272. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3278 line 578
273. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3279 line 581
274. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3279 line 582
275. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3280 line 585
276. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3280 line 586
277. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3281 line 589
278. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3281 line 590
279. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3282 line 593
280. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3282 line 594
281. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3283 line 597
282. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3283 line 598
283. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3284 line 601
284. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3284 line 602
285. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3285 line 605
286. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3285 line 606
287. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3286 line 609
288. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3286 line 610
289. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3287 line 613
290. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3287 line 614
291. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3288 line 617
292. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3288 line 618
293. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3289 line 621
294. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3289 line 622
295. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3290 line 625
296. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3290 line 626
297. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3291 line 629
298. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3291 line 630
299. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3292 line 633
300. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3292 line 634
301. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3293 line 637
302. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3293 line 638
303. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3294 line 641
304. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3294 line 642
305. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3295 line 645
306. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3295 line 646
307. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3296 line 649
308. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3296 line 650
309. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3297 line 653
310. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3297 line 654
311. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3298 line 657
312. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3298 line 658
313. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3299 line 661
314. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3299 line 662
315. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3300 line 665
316. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3300 line 666
317. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3301 line 669
318. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3301 line 670
319. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3302 line 673
320. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3302 line 674
321. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3303 line 677
322. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3303 line 678
323. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3304 line 681
324. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3304 line 682
325. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3305 line 685
326. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3305 line 686
327. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3306 line 689
328. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3306 line 690
329. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3307 line 693
330. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3307 line 694
331. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3308 line 697
332. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3308 line 698
333. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3309 line 701
334. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3309 line 702
335. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3310 line 705
336. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3310 line 706
337. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3311 line 709
338. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3311 line 710
339. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3312 line 713
340. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3312 line 714
341. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3313 line 717
342. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3313 line 718
343. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3314 line 721
344. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3314 line 722
345. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3315 line 725
346. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3315 line 726
347. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3316 line 729
348. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3316 line 730
349. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3317 line 733
350. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3317 line 734
351. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3318 line 737
352. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3318 line 738
353. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3319 line 741
354. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3319 line 742
355. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3320 line 745
356. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3320 line 746
357. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3321 line 749
358. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3321 line 750
359. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3322 line 753
360. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3322 line 754
361. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3323 line 757
362. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3323 line 758
363. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3324 line 761
364. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3324 line 762
365. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3325 line 765
366. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3325 line 766
367. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3326 line 775
368. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3326 line 776
369. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3327 line 779
370. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3327 line 780
371. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3328 line 783
372. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3328 line 784
373. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3329 line 787
374. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3329 line 788
375. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3330 line 791
376. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3330 line 792
377. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3331 line 795
378. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3331 line 796
379. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3332 line 799
380. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3332 line 800
381. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3333 line 803
382. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3333 line 804
383. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3334 line 807
384. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3334 line 808
385. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3335 line 811
386. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3335 line 812
387. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_64 line 815
388. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_74 line 818
389. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_84 line 821
390. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_92 line 824
391. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_98 line 827
392. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_102 line 830
393. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_102 line 833
394. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_106 line 837
395. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_106 line 840
396. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_110 line 844
397. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_110 line 847
398. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_114 line 851
399. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_114 line 854
400. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_118 line 858
401. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_118 line 861
402. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_122 line 865
403. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_122 line 868
404. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_126 line 872
405. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_126 line 875
406. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_130 line 879
407. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_130 line 882
408. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_134 line 886
409. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_134 line 889
410. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_138 line 893
411. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_138 line 896
412. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_142 line 900
413. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_142 line 903
414. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_146 line 907
415. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_146 line 910
416. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_150 line 914