OAI/Geometry/CubicTorus/Profiles/ValueEnclosures1165To1383.lean

GitHub source file

437 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1165 line 19
2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1165 line 20
3. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1166 line 23
4. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1166 line 24
5. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1167 line 27
6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1167 line 28
7. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1168 line 31
8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1168 line 32
9. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1169 line 35
10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1169 line 36
11. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1170 line 39
12. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1170 line 40
13. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1171 line 43
14. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1171 line 44
15. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1172 line 47
16. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1172 line 48
17. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1173 line 51
18. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1173 line 52
19. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1174 line 55
20. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1174 line 56
21. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1175 line 59
22. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1175 line 60
23. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1176 line 63
24. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1176 line 64
25. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1177 line 67
26. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1177 line 68
27. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1178 line 71
28. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1178 line 72
29. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1179 line 75
30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1179 line 76
31. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1180 line 79
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1180 line 80
33. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1181 line 83
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1181 line 84
35. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1182 line 87
36. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1182 line 88
37. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1183 line 91
38. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1183 line 92
39. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1184 line 95
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1184 line 96
41. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1185 line 99
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1185 line 100
43. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1186 line 103
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1186 line 104
45. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1187 line 107
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1187 line 108
47. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1188 line 117
48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1188 line 118
49. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1189 line 121
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1189 line 122
51. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1190 line 125
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1190 line 126
53. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1191 line 129
54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1191 line 130
55. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1192 line 133
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1192 line 134
57. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1193 line 137
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1193 line 138
59. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1194 line 141
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1194 line 142
61. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1195 line 145
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1195 line 146
63. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1196 line 149
64. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1196 line 150
65. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1197 line 153
66. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1197 line 154
67. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1198 line 157
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1198 line 158
69. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1199 line 161
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1199 line 162
71. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1200 line 165
72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1200 line 166
73. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1201 line 169
74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1201 line 170
75. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1202 line 173
76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1202 line 174
77. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1203 line 183
78. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1203 line 184
79. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1204 line 187
80. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1204 line 188
81. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1205 line 191
82. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1205 line 192
83. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1206 line 195
84. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1206 line 196
85. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1207 line 199
86. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1207 line 200
87. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1208 line 203
88. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1208 line 204
89. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1209 line 207
90. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1209 line 208
91. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1210 line 211
92. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1210 line 212
93. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1211 line 215
94. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1211 line 216
95. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1212 line 219
96. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1212 line 220
97. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1213 line 223
98. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1213 line 224
99. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1214 line 227
100. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1214 line 228
101. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1215 line 231
102. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1215 line 232
103. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1216 line 235
104. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1216 line 236
105. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1217 line 239
106. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1217 line 240
107. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1218 line 243
108. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1218 line 244
109. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1219 line 247
110. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1219 line 248
111. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1220 line 251
112. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1220 line 252
113. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1221 line 255
114. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1221 line 256
115. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1222 line 259
116. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1222 line 260
117. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1223 line 263
118. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1223 line 264
119. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1224 line 267
120. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1224 line 268
121. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1225 line 271
122. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1225 line 272
123. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1226 line 275
124. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1226 line 276
125. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1227 line 279
126. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1227 line 280
127. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1228 line 283
128. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1228 line 284
129. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1229 line 287
130. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1229 line 288
131. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1230 line 291
132. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1230 line 292
133. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1231 line 295
134. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1231 line 296
135. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1232 line 299
136. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1232 line 300
137. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1233 line 303
138. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1233 line 304
139. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1234 line 307
140. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1234 line 308
141. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1235 line 311
142. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1235 line 312
143. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1236 line 315
144. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1236 line 316
145. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1237 line 319
146. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1237 line 320
147. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1238 line 323
148. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1238 line 324
149. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1239 line 327
150. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1239 line 328
151. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1240 line 331
152. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1240 line 332
153. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1241 line 335
154. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1241 line 336
155. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1242 line 339
156. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1242 line 340
157. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1243 line 343
158. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1243 line 344
159. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1244 line 347
160. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1244 line 348
161. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1245 line 351
162. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1245 line 352
163. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1246 line 355
164. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1246 line 356
165. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1247 line 359
166. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1247 line 360
167. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1248 line 363
168. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1248 line 364
169. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1249 line 367
170. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1249 line 368
171. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1250 line 371
172. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1250 line 372
173. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1251 line 375
174. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1251 line 376
175. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1252 line 379
176. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1252 line 380
177. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1253 line 383
178. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1253 line 384
179. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1254 line 387
180. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1254 line 388
181. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1255 line 391
182. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1255 line 392
183. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1256 line 395
184. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1256 line 396
185. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1257 line 399
186. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1257 line 400
187. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1258 line 409
188. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1258 line 410
189. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1259 line 413
190. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1259 line 414
191. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1260 line 417
192. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1260 line 418
193. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1261 line 421
194. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1261 line 422
195. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1262 line 425
196. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1262 line 426
197. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1263 line 429
198. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1263 line 430
199. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1264 line 433
200. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1264 line 434
201. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1265 line 437
202. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1265 line 438
203. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1266 line 441
204. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1266 line 442
205. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1267 line 445
206. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1267 line 446
207. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1268 line 449
208. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1268 line 450
209. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1269 line 453
210. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1269 line 454
211. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1270 line 457
212. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1270 line 458
213. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1271 line 461
214. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1271 line 462
215. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1272 line 465
216. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1272 line 466
217. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1273 line 469
218. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1273 line 470
219. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1274 line 473
220. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1274 line 474
221. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1275 line 477
222. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1275 line 478
223. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1276 line 481
224. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1276 line 482
225. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1277 line 485
226. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1277 line 486
227. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1278 line 489
228. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1278 line 490
229. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1279 line 493
230. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1279 line 494
231. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1280 line 497
232. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1280 line 498
233. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1281 line 501
234. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1281 line 502
235. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1282 line 505
236. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1282 line 506
237. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1283 line 509
238. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1283 line 510
239. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1284 line 513
240. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1284 line 514
241. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1285 line 517
242. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1285 line 518
243. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1286 line 521
244. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1286 line 522
245. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1287 line 525
246. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1287 line 526
247. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1288 line 529
248. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1288 line 530
249. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1289 line 533
250. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1289 line 534
251. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1290 line 537
252. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1290 line 538
253. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1291 line 541
254. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1291 line 542
255. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1292 line 545
256. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1292 line 546
257. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1293 line 549
258. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1293 line 550
259. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1294 line 553
260. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1294 line 554
261. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1295 line 557
262. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1295 line 558
263. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1296 line 561
264. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1296 line 562
265. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1297 line 565
266. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1297 line 566
267. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1298 line 569
268. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1298 line 570
269. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1299 line 573
270. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1299 line 574
271. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1300 line 577
272. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1300 line 578
273. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1301 line 581
274. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1301 line 582
275. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1302 line 585
276. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1302 line 586
277. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1303 line 589
278. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1303 line 590
279. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1304 line 593
280. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1304 line 594
281. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1305 line 597
282. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1305 line 598
283. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1306 line 601
284. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1306 line 602
285. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1307 line 605
286. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1307 line 606
287. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1308 line 609
288. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1308 line 610
289. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1309 line 613
290. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1309 line 614
291. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1310 line 617
292. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1310 line 618
293. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1311 line 621
294. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1311 line 622
295. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1312 line 625
296. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1312 line 626
297. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1313 line 629
298. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1313 line 630
299. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1314 line 633
300. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1314 line 634
301. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1315 line 637
302. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1315 line 638
303. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1316 line 641
304. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1316 line 642
305. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1317 line 645
306. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1317 line 646
307. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1318 line 649
308. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1318 line 650
309. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1319 line 653
310. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1319 line 654
311. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1320 line 657
312. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1320 line 658
313. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1321 line 661
314. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1321 line 662
315. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1322 line 665
316. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1322 line 666
317. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1323 line 669
318. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1323 line 670
319. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1324 line 673
320. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1324 line 674
321. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1325 line 677
322. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1325 line 678
323. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1326 line 681
324. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1326 line 682
325. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1327 line 685
326. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1327 line 686
327. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1328 line 689
328. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1328 line 690
329. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1329 line 693
330. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1329 line 694
331. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1330 line 697
332. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1330 line 698
333. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1331 line 701
334. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1331 line 702
335. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1332 line 705
336. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1332 line 706
337. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1333 line 709
338. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1333 line 710
339. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1334 line 713
340. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1334 line 714
341. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1335 line 717
342. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1335 line 718
343. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1336 line 721
344. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1336 line 722
345. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1337 line 725
346. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1337 line 726
347. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1338 line 729
348. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1338 line 730
349. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1339 line 733
350. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1339 line 734
351. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1340 line 737
352. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1340 line 738
353. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1341 line 741
354. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1341 line 742
355. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1342 line 745
356. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1342 line 746
357. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1343 line 749
358. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1343 line 750
359. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1344 line 753
360. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1344 line 754
361. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1345 line 757
362. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1345 line 758
363. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1346 line 761
364. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1346 line 762
365. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1347 line 765
366. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1347 line 766
367. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1348 line 769
368. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1348 line 770
369. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1349 line 773
370. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1349 line 774
371. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1350 line 777
372. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1350 line 778
373. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1351 line 781
374. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1351 line 782
375. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1352 line 785
376. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1352 line 786
377. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1353 line 789
378. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1353 line 790
379. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1354 line 793
380. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1354 line 794
381. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1355 line 797
382. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1355 line 798
383. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1356 line 801
384. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1356 line 802
385. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1357 line 805
386. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1357 line 806
387. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1358 line 809
388. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1358 line 810
389. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1359 line 813
390. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1359 line 814
391. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1360 line 817
392. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1360 line 818
393. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1361 line 821
394. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1361 line 822
395. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1362 line 825
396. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1362 line 826
397. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1363 line 829
398. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1363 line 830
399. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1364 line 833
400. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1364 line 834
401. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1365 line 837
402. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1365 line 838
403. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1366 line 841
404. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1366 line 842
405. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1367 line 845
406. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1367 line 846
407. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1368 line 849
408. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1368 line 850
409. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1369 line 859
410. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1369 line 860
411. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1370 line 863
412. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1370 line 864
413. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1371 line 867
414. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1371 line 868
415. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1372 line 871
416. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1372 line 872
417. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1373 line 875
418. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1373 line 876
419. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1374 line 879
420. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1374 line 880
421. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1375 line 883
422. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1375 line 884
423. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1376 line 887
424. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1376 line 888
425. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1377 line 891
426. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1377 line 892
427. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1378 line 895
428. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1378 line 896
429. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1379 line 899
430. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1379 line 900
431. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1380 line 903
432. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1380 line 904
433. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1381 line 907
434. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1381 line 908
435. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1382 line 911
436. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1382 line 912
437. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1383 line 915