OAI/Geometry/CubicTorus/Profiles/ValueEnclosures2042To2262.lean

GitHub source file

441 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2042 line 19
2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2042 line 20
3. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2043 line 23
4. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2043 line 24
5. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2044 line 27
6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2044 line 28
7. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2045 line 31
8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2045 line 32
9. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2046 line 35
10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2046 line 36
11. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2047 line 39
12. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2047 line 40
13. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2048 line 43
14. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2048 line 44
15. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2049 line 47
16. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2049 line 48
17. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2050 line 51
18. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2050 line 52
19. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2051 line 55
20. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2051 line 56
21. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2052 line 59
22. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2052 line 60
23. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2053 line 63
24. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2053 line 64
25. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2054 line 67
26. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2054 line 68
27. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2055 line 71
28. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2055 line 72
29. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2056 line 75
30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2056 line 76
31. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2057 line 79
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2057 line 80
33. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2058 line 83
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2058 line 84
35. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2059 line 87
36. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2059 line 88
37. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2060 line 91
38. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2060 line 92
39. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2061 line 95
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2061 line 96
41. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2062 line 99
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2062 line 100
43. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2063 line 103
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2063 line 104
45. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2064 line 107
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2064 line 108
47. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2065 line 111
48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2065 line 112
49. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2066 line 115
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2066 line 116
51. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2067 line 119
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2067 line 120
53. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2068 line 123
54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2068 line 124
55. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2069 line 127
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2069 line 128
57. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2070 line 131
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2070 line 132
59. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2071 line 135
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2071 line 136
61. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2072 line 139
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2072 line 140
63. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2073 line 143
64. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2073 line 144
65. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2074 line 147
66. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2074 line 148
67. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2075 line 151
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2075 line 152
69. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2076 line 155
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2076 line 156
71. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2077 line 159
72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2077 line 160
73. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2078 line 163
74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2078 line 164
75. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2079 line 167
76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2079 line 168
77. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2080 line 171
78. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2080 line 172
79. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2081 line 175
80. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2081 line 176
81. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2082 line 179
82. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2082 line 180
83. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2083 line 183
84. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2083 line 184
85. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2084 line 187
86. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2084 line 188
87. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2085 line 191
88. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2085 line 192
89. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2086 line 195
90. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2086 line 196
91. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2087 line 199
92. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2087 line 200
93. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2088 line 203
94. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2088 line 204
95. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2089 line 207
96. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2089 line 208
97. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2090 line 211
98. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2090 line 212
99. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2091 line 215
100. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2091 line 216
101. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2092 line 219
102. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2092 line 220
103. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2093 line 229
104. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2093 line 230
105. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2094 line 233
106. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2094 line 234
107. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2095 line 237
108. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2095 line 238
109. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2096 line 241
110. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2096 line 242
111. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2097 line 245
112. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2097 line 246
113. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2098 line 249
114. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2098 line 250
115. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2099 line 253
116. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2099 line 254
117. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2100 line 257
118. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2100 line 258
119. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2101 line 261
120. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2101 line 262
121. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2102 line 265
122. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2102 line 266
123. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2103 line 269
124. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2103 line 270
125. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2104 line 273
126. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2104 line 274
127. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2105 line 277
128. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2105 line 278
129. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2106 line 281
130. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2106 line 282
131. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2107 line 285
132. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2107 line 286
133. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2108 line 295
134. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2108 line 296
135. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2109 line 299
136. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2109 line 300
137. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2110 line 303
138. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2110 line 304
139. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2111 line 307
140. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2111 line 308
141. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2112 line 311
142. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2112 line 312
143. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2113 line 315
144. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2113 line 316
145. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2114 line 319
146. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2114 line 320
147. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2115 line 323
148. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2115 line 324
149. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2116 line 327
150. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2116 line 328
151. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2117 line 331
152. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2117 line 332
153. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2118 line 335
154. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2118 line 336
155. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2119 line 339
156. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2119 line 340
157. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2120 line 343
158. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2120 line 344
159. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2121 line 347
160. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2121 line 348
161. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2122 line 351
162. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2122 line 352
163. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2123 line 355
164. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2123 line 356
165. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2124 line 359
166. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2124 line 360
167. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2125 line 363
168. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2125 line 364
169. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2126 line 367
170. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2126 line 368
171. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2127 line 371
172. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2127 line 372
173. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2128 line 375
174. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2128 line 376
175. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2129 line 379
176. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2129 line 380
177. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2130 line 383
178. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2130 line 384
179. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2131 line 387
180. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2131 line 388
181. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2132 line 391
182. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2132 line 392
183. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2133 line 395
184. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2133 line 396
185. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2134 line 399
186. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2134 line 400
187. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2135 line 403
188. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2135 line 404
189. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2136 line 407
190. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2136 line 408
191. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2137 line 411
192. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2137 line 412
193. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2138 line 415
194. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2138 line 416
195. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2139 line 419
196. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2139 line 420
197. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2140 line 423
198. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2140 line 424
199. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2141 line 427
200. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2141 line 428
201. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2142 line 431
202. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2142 line 432
203. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2143 line 435
204. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2143 line 436
205. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2144 line 439
206. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2144 line 440
207. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2145 line 443
208. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2145 line 444
209. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2146 line 447
210. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2146 line 448
211. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2147 line 451
212. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2147 line 452
213. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2148 line 455
214. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2148 line 456
215. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2149 line 459
216. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2149 line 460
217. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2150 line 463
218. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2150 line 464
219. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2151 line 467
220. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2151 line 468
221. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2152 line 471
222. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2152 line 472
223. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2153 line 475
224. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2153 line 476
225. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2154 line 479
226. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2154 line 480
227. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2155 line 483
228. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2155 line 484
229. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2156 line 487
230. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2156 line 488
231. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2157 line 491
232. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2157 line 492
233. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2158 line 495
234. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2158 line 496
235. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2159 line 499
236. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2159 line 500
237. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2160 line 503
238. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2160 line 504
239. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2161 line 507
240. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2161 line 508
241. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2162 line 511
242. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2162 line 512
243. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2163 line 521
244. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2163 line 522
245. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2164 line 525
246. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2164 line 526
247. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2165 line 529
248. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2165 line 530
249. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2166 line 533
250. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2166 line 534
251. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2167 line 537
252. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2167 line 538
253. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2168 line 541
254. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2168 line 542
255. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2169 line 545
256. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2169 line 546
257. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2170 line 549
258. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2170 line 550
259. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2171 line 553
260. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2171 line 554
261. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2172 line 557
262. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2172 line 558
263. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2173 line 561
264. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2173 line 562
265. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2174 line 565
266. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2174 line 566
267. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2175 line 569
268. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2175 line 570
269. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2176 line 573
270. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2176 line 574
271. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2177 line 577
272. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2177 line 578
273. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2178 line 581
274. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2178 line 582
275. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2179 line 585
276. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2179 line 586
277. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2180 line 589
278. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2180 line 590
279. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2181 line 593
280. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2181 line 594
281. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2182 line 597
282. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2182 line 598
283. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2183 line 601
284. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2183 line 602
285. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2184 line 605
286. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2184 line 606
287. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2185 line 609
288. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2185 line 610
289. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2186 line 613
290. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2186 line 614
291. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2187 line 617
292. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2187 line 618
293. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2188 line 621
294. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2188 line 622
295. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2189 line 625
296. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2189 line 626
297. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2190 line 629
298. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2190 line 630
299. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2191 line 633
300. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2191 line 634
301. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2192 line 637
302. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2192 line 638
303. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2193 line 641
304. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2193 line 642
305. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2194 line 645
306. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2194 line 646
307. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2195 line 649
308. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2195 line 650
309. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2196 line 653
310. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2196 line 654
311. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2197 line 657
312. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2197 line 658
313. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2198 line 661
314. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2198 line 662
315. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2199 line 665
316. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2199 line 666
317. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2200 line 669
318. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2200 line 670
319. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2201 line 673
320. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2201 line 674
321. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2202 line 677
322. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2202 line 678
323. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2203 line 681
324. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2203 line 682
325. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2204 line 685
326. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2204 line 686
327. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2205 line 689
328. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2205 line 690
329. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2206 line 693
330. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2206 line 694
331. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2207 line 697
332. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2207 line 698
333. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2208 line 701
334. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2208 line 702
335. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2209 line 705
336. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2209 line 706
337. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2210 line 709
338. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2210 line 710
339. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2211 line 713
340. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2211 line 714
341. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2212 line 717
342. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2212 line 718
343. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2213 line 721
344. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2213 line 722
345. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2214 line 725
346. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2214 line 726
347. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2215 line 729
348. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2215 line 730
349. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2216 line 733
350. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2216 line 734
351. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2217 line 737
352. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2217 line 738
353. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2218 line 741
354. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2218 line 742
355. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2219 line 745
356. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2219 line 746
357. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2220 line 749
358. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2220 line 750
359. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2221 line 753
360. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2221 line 754
361. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2222 line 757
362. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2222 line 758
363. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2223 line 761
364. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2223 line 762
365. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2224 line 765
366. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2224 line 766
367. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2225 line 769
368. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2225 line 770
369. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2226 line 773
370. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2226 line 774
371. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2227 line 777
372. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2227 line 778
373. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2228 line 781
374. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2228 line 782
375. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2229 line 785
376. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2229 line 786
377. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2230 line 789
378. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2230 line 790
379. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2231 line 793
380. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2231 line 794
381. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2232 line 797
382. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2232 line 798
383. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2233 line 801
384. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2233 line 802
385. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2234 line 805
386. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2234 line 806
387. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2235 line 809
388. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2235 line 810
389. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2236 line 813
390. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2236 line 814
391. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2237 line 817
392. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2237 line 818
393. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2238 line 821
394. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2238 line 822
395. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2239 line 825
396. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2239 line 826
397. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2240 line 829
398. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2240 line 830
399. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2241 line 833
400. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2241 line 834
401. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2242 line 837
402. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2242 line 838
403. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2243 line 841
404. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2243 line 842
405. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2244 line 845
406. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2244 line 846
407. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2245 line 849
408. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2245 line 850
409. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2246 line 853
410. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2246 line 854
411. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2247 line 857
412. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2247 line 858
413. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2248 line 861
414. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2248 line 862
415. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2249 line 865
416. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2249 line 866
417. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2250 line 869
418. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2250 line 870
419. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2251 line 873
420. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2251 line 874
421. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2252 line 877
422. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2252 line 878
423. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2253 line 881
424. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2253 line 882
425. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2254 line 885
426. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2254 line 886
427. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2255 line 889
428. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2255 line 890
429. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2256 line 893
430. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2256 line 894
431. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2257 line 897
432. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2257 line 898
433. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2258 line 901
434. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2258 line 902
435. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2259 line 905
436. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2259 line 906
437. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2260 line 909
438. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2260 line 910
439. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2261 line 913
440. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2261 line 914
441. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2262 line 917