OAI/Geometry/CubicTorus/Profiles/ValueEnclosures726To944.lean

GitHub source file

438 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b725 line 18
2. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e726 line 21
3. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b726 line 22
4. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e727 line 25
5. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b727 line 26
6. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e728 line 29
7. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b728 line 30
8. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e729 line 33
9. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b729 line 34
10. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e730 line 37
11. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b730 line 38
12. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e731 line 41
13. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b731 line 42
14. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e732 line 45
15. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b732 line 46
16. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e733 line 49
17. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b733 line 50
18. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e734 line 53
19. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b734 line 54
20. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e735 line 57
21. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b735 line 58
22. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e736 line 61
23. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b736 line 62
24. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e737 line 65
25. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b737 line 66
26. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e738 line 69
27. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b738 line 70
28. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e739 line 73
29. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b739 line 74
30. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e740 line 77
31. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b740 line 78
32. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e741 line 81
33. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b741 line 82
34. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e742 line 85
35. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b742 line 86
36. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e743 line 95
37. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b743 line 96
38. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e744 line 99
39. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b744 line 100
40. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e745 line 103
41. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b745 line 104
42. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e746 line 107
43. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b746 line 108
44. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e747 line 111
45. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b747 line 112
46. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e748 line 115
47. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b748 line 116
48. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e749 line 119
49. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b749 line 120
50. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e750 line 123
51. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b750 line 124
52. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e751 line 127
53. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b751 line 128
54. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e752 line 131
55. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b752 line 132
56. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e753 line 135
57. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b753 line 136
58. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e754 line 139
59. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b754 line 140
60. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e755 line 143
61. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b755 line 144
62. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e756 line 147
63. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b756 line 148
64. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e757 line 151
65. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b757 line 152
66. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e758 line 155
67. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b758 line 156
68. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e759 line 159
69. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b759 line 160
70. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e760 line 163
71. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b760 line 164
72. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e761 line 167
73. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b761 line 168
74. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e762 line 171
75. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b762 line 172
76. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e763 line 175
77. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b763 line 176
78. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e764 line 179
79. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b764 line 180
80. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e765 line 183
81. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b765 line 184
82. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e766 line 187
83. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b766 line 188
84. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e767 line 191
85. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b767 line 192
86. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e768 line 195
87. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b768 line 196
88. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e769 line 199
89. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b769 line 200
90. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e770 line 203
91. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b770 line 204
92. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e771 line 207
93. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b771 line 208
94. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e772 line 211
95. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b772 line 212
96. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e773 line 215
97. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b773 line 216
98. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e774 line 219
99. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b774 line 220
100. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e775 line 223
101. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b775 line 224
102. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e776 line 227
103. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b776 line 228
104. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e777 line 231
105. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b777 line 232
106. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e778 line 235
107. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b778 line 236
108. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e779 line 239
109. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b779 line 240
110. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e780 line 243
111. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b780 line 244
112. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e781 line 247
113. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b781 line 248
114. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e782 line 251
115. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b782 line 252
116. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e783 line 255
117. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b783 line 256
118. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e784 line 259
119. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b784 line 260
120. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e785 line 263
121. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b785 line 264
122. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e786 line 267
123. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b786 line 268
124. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e787 line 271
125. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b787 line 272
126. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e788 line 275
127. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b788 line 276
128. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e789 line 279
129. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b789 line 280
130. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e790 line 283
131. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b790 line 284
132. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e791 line 287
133. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b791 line 288
134. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e792 line 291
135. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b792 line 292
136. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e793 line 295
137. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b793 line 296
138. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e794 line 299
139. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b794 line 300
140. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e795 line 303
141. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b795 line 304
142. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e796 line 307
143. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b796 line 308
144. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e797 line 311
145. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b797 line 312
146. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e798 line 315
147. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b798 line 316
148. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e799 line 319
149. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b799 line 320
150. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e800 line 323
151. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b800 line 324
152. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e801 line 327
153. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b801 line 328
154. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e802 line 331
155. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b802 line 332
156. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e803 line 335
157. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b803 line 336
158. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e804 line 339
159. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b804 line 340
160. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e805 line 343
161. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b805 line 344
162. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e806 line 347
163. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b806 line 348
164. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e807 line 351
165. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b807 line 352
166. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e808 line 355
167. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b808 line 356
168. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e809 line 359
169. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b809 line 360
170. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e810 line 363
171. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b810 line 364
172. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e811 line 367
173. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b811 line 368
174. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e812 line 371
175. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b812 line 372
176. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e813 line 375
177. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b813 line 376
178. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e814 line 379
179. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b814 line 380
180. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e815 line 383
181. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b815 line 384
182. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e816 line 387
183. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b816 line 388
184. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e817 line 391
185. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b817 line 392
186. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e818 line 395
187. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b818 line 396
188. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e819 line 399
189. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b819 line 400
190. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e820 line 409
191. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b820 line 410
192. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e821 line 413
193. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b821 line 414
194. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e822 line 417
195. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b822 line 418
196. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e823 line 421
197. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b823 line 422
198. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e824 line 425
199. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b824 line 426
200. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e825 line 429
201. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b825 line 430
202. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e826 line 433
203. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b826 line 434
204. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e827 line 437
205. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b827 line 438
206. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e828 line 441
207. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b828 line 442
208. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e829 line 445
209. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b829 line 446
210. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e830 line 449
211. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b830 line 450
212. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e831 line 453
213. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b831 line 454
214. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e832 line 457
215. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b832 line 458
216. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e833 line 461
217. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b833 line 462
218. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e834 line 465
219. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b834 line 466
220. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e835 line 475
221. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b835 line 476
222. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e836 line 479
223. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b836 line 480
224. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e837 line 483
225. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b837 line 484
226. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e838 line 487
227. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b838 line 488
228. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e839 line 491
229. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b839 line 492
230. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e840 line 495
231. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b840 line 496
232. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e841 line 499
233. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b841 line 500
234. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e842 line 503
235. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b842 line 504
236. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e843 line 507
237. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b843 line 508
238. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e844 line 511
239. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b844 line 512
240. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e845 line 515
241. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b845 line 516
242. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e846 line 519
243. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b846 line 520
244. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e847 line 523
245. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b847 line 524
246. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e848 line 527
247. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b848 line 528
248. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e849 line 531
249. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b849 line 532
250. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e850 line 535
251. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b850 line 536
252. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e851 line 539
253. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b851 line 540
254. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e852 line 543
255. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b852 line 544
256. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e853 line 547
257. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b853 line 548
258. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e854 line 551
259. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b854 line 552
260. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e855 line 555
261. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b855 line 556
262. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e856 line 559
263. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b856 line 560
264. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e857 line 563
265. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b857 line 564
266. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e858 line 567
267. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b858 line 568
268. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e859 line 571
269. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b859 line 572
270. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e860 line 575
271. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b860 line 576
272. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e861 line 579
273. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b861 line 580
274. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e862 line 583
275. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b862 line 584
276. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e863 line 587
277. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b863 line 588
278. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e864 line 591
279. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b864 line 592
280. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e865 line 595
281. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b865 line 596
282. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e866 line 599
283. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b866 line 600
284. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e867 line 603
285. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b867 line 604
286. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e868 line 607
287. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b868 line 608
288. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e869 line 611
289. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b869 line 612
290. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e870 line 615
291. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b870 line 616
292. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e871 line 619
293. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b871 line 620
294. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e872 line 623
295. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b872 line 624
296. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e873 line 627
297. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b873 line 628
298. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e874 line 631
299. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b874 line 632
300. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e875 line 635
301. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b875 line 636
302. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e876 line 639
303. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b876 line 640
304. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e877 line 643
305. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b877 line 644
306. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e878 line 647
307. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b878 line 648
308. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e879 line 651
309. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b879 line 652
310. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e880 line 655
311. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b880 line 656
312. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e881 line 659
313. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b881 line 660
314. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e882 line 663
315. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b882 line 664
316. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e883 line 667
317. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b883 line 668
318. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e884 line 671
319. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b884 line 672
320. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e885 line 675
321. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b885 line 676
322. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e886 line 679
323. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b886 line 680
324. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e887 line 683
325. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b887 line 684
326. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e888 line 687
327. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b888 line 688
328. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e889 line 691
329. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b889 line 692
330. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e890 line 701
331. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b890 line 702
332. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e891 line 705
333. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b891 line 706
334. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e892 line 709
335. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b892 line 710
336. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e893 line 713
337. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b893 line 714
338. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e894 line 717
339. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b894 line 718
340. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e895 line 721
341. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b895 line 722
342. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e896 line 725
343. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b896 line 726
344. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e897 line 729
345. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b897 line 730
346. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e898 line 733
347. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b898 line 734
348. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e899 line 737
349. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b899 line 738
350. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e900 line 741
351. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b900 line 742
352. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e901 line 745
353. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b901 line 746
354. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e902 line 749
355. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b902 line 750
356. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e903 line 753
357. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b903 line 754
358. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e904 line 757
359. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b904 line 758
360. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e905 line 761
361. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b905 line 762
362. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e906 line 765
363. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b906 line 766
364. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e907 line 769
365. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b907 line 770
366. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e908 line 773
367. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b908 line 774
368. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e909 line 777
369. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b909 line 778
370. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e910 line 781
371. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b910 line 782
372. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e911 line 785
373. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b911 line 786
374. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e912 line 789
375. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b912 line 790
376. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e913 line 793
377. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b913 line 794
378. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e914 line 797
379. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b914 line 798
380. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e915 line 801
381. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b915 line 802
382. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e916 line 805
383. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b916 line 806
384. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e917 line 809
385. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b917 line 810
386. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e918 line 813
387. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b918 line 814
388. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e919 line 817
389. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b919 line 818
390. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e920 line 821
391. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b920 line 822
392. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e921 line 825
393. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b921 line 826
394. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e922 line 829
395. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b922 line 830
396. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e923 line 833
397. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b923 line 834
398. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e924 line 837
399. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b924 line 838
400. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e925 line 841
401. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b925 line 842
402. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e926 line 845
403. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b926 line 846
404. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e927 line 849
405. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b927 line 850
406. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e928 line 853
407. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b928 line 854
408. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e929 line 857
409. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b929 line 858
410. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e930 line 861
411. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b930 line 862
412. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e931 line 865
413. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b931 line 866
414. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e932 line 869
415. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b932 line 870
416. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e933 line 873
417. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b933 line 874
418. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e934 line 877
419. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b934 line 878
420. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e935 line 881
421. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b935 line 882
422. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e936 line 885
423. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b936 line 886
424. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e937 line 889
425. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b937 line 890
426. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e938 line 893
427. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b938 line 894
428. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e939 line 897
429. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b939 line 898
430. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e940 line 901
431. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b940 line 902
432. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e941 line 905
433. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b941 line 906
434. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e942 line 909
435. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b942 line 910
436. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e943 line 913
437. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b943 line 914
438. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e944 line 917