OAI/Analysis/PlanarPacking/Roots.lean

GitHub source file

3269 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpPlanar.rootPhase line 14
2. lemma OAI.SharpPlanar.rootPhase_eq_pow line 16
3. lemma OAI.SharpPlanar.rootPhase_add line 22
4. lemma OAI.SharpPlanar.rootPhase_periodic line 29
5. lemma OAI.SharpPlanar.rootPhase_mod line 35
6. lemma OAI.SharpPlanar.rootPhase_cos line 39
7. def OAI.SharpPlanar.IntegerRoots.fact0 line 53
8. lemma OAI.SharpPlanar.IntegerRoots.fact0_check line 54
9. def OAI.SharpPlanar.IntegerRoots.fact1 line 55
10. lemma OAI.SharpPlanar.IntegerRoots.fact1_check line 56
11. def OAI.SharpPlanar.IntegerRoots.fact2 line 57
12. lemma OAI.SharpPlanar.IntegerRoots.fact2_check line 58
13. def OAI.SharpPlanar.IntegerRoots.fact3 line 59
14. lemma OAI.SharpPlanar.IntegerRoots.fact3_check line 60
15. def OAI.SharpPlanar.IntegerRoots.fact4 line 61
16. lemma OAI.SharpPlanar.IntegerRoots.fact4_check line 62
17. def OAI.SharpPlanar.IntegerRoots.fact5 line 63
18. lemma OAI.SharpPlanar.IntegerRoots.fact5_check line 64
19. def OAI.SharpPlanar.IntegerRoots.fact6 line 65
20. lemma OAI.SharpPlanar.IntegerRoots.fact6_check line 66
21. def OAI.SharpPlanar.IntegerRoots.fact7 line 67
22. lemma OAI.SharpPlanar.IntegerRoots.fact7_check line 68
23. def OAI.SharpPlanar.IntegerRoots.fact8 line 69
24. lemma OAI.SharpPlanar.IntegerRoots.fact8_check line 70
25. def OAI.SharpPlanar.IntegerRoots.fact9 line 71
26. lemma OAI.SharpPlanar.IntegerRoots.fact9_check line 72
27. def OAI.SharpPlanar.IntegerRoots.fact10 line 73
28. lemma OAI.SharpPlanar.IntegerRoots.fact10_check line 74
29. def OAI.SharpPlanar.IntegerRoots.fact11 line 75
30. lemma OAI.SharpPlanar.IntegerRoots.fact11_check line 76
31. def OAI.SharpPlanar.IntegerRoots.fact12 line 77
32. lemma OAI.SharpPlanar.IntegerRoots.fact12_check line 78
33. def OAI.SharpPlanar.IntegerRoots.fact13 line 79
34. lemma OAI.SharpPlanar.IntegerRoots.fact13_check line 80
35. def OAI.SharpPlanar.IntegerRoots.fact14 line 81
36. lemma OAI.SharpPlanar.IntegerRoots.fact14_check line 82
37. def OAI.SharpPlanar.IntegerRoots.fact15 line 83
38. lemma OAI.SharpPlanar.IntegerRoots.fact15_check line 84
39. def OAI.SharpPlanar.IntegerRoots.fact16 line 85
40. lemma OAI.SharpPlanar.IntegerRoots.fact16_check line 86
41. def OAI.SharpPlanar.IntegerRoots.fact17 line 87
42. lemma OAI.SharpPlanar.IntegerRoots.fact17_check line 88
43. def OAI.SharpPlanar.IntegerRoots.fact18 line 89
44. lemma OAI.SharpPlanar.IntegerRoots.fact18_check line 90
45. def OAI.SharpPlanar.IntegerRoots.fact19 line 91
46. lemma OAI.SharpPlanar.IntegerRoots.fact19_check line 92
47. def OAI.SharpPlanar.IntegerRoots.fact20 line 93
48. lemma OAI.SharpPlanar.IntegerRoots.fact20_check line 94
49. def OAI.SharpPlanar.IntegerRoots.fact21 line 95
50. lemma OAI.SharpPlanar.IntegerRoots.fact21_check line 96
51. def OAI.SharpPlanar.IntegerRoots.fact22 line 97
52. lemma OAI.SharpPlanar.IntegerRoots.fact22_check line 98
53. def OAI.SharpPlanar.IntegerRoots.fact23 line 99
54. lemma OAI.SharpPlanar.IntegerRoots.fact23_check line 100
55. def OAI.SharpPlanar.IntegerRoots.fact24 line 101
56. lemma OAI.SharpPlanar.IntegerRoots.fact24_check line 102
57. def OAI.SharpPlanar.IntegerRoots.fact25 line 103
58. lemma OAI.SharpPlanar.IntegerRoots.fact25_check line 104
59. def OAI.SharpPlanar.IntegerRoots.fact26 line 105
60. lemma OAI.SharpPlanar.IntegerRoots.fact26_check line 106
61. def OAI.SharpPlanar.IntegerRoots.fact27 line 107
62. lemma OAI.SharpPlanar.IntegerRoots.fact27_check line 108
63. def OAI.SharpPlanar.IntegerRoots.fact28 line 109
64. lemma OAI.SharpPlanar.IntegerRoots.fact28_check line 110
65. def OAI.SharpPlanar.IntegerRoots.fact29 line 111
66. lemma OAI.SharpPlanar.IntegerRoots.fact29_check line 112
67. def OAI.SharpPlanar.IntegerRoots.fact30 line 113
68. lemma OAI.SharpPlanar.IntegerRoots.fact30_check line 114
69. def OAI.SharpPlanar.IntegerRoots.fact31 line 115
70. lemma OAI.SharpPlanar.IntegerRoots.fact31_check line 116
71. def OAI.SharpPlanar.IntegerRoots.fact32 line 117
72. lemma OAI.SharpPlanar.IntegerRoots.fact32_check line 118
73. def OAI.SharpPlanar.IntegerRoots.phaseInput line 119
74. lemma OAI.SharpPlanar.IntegerRoots.phaseInput_contains line 120
75. def OAI.SharpPlanar.IntegerRoots.small line 126
76. lemma OAI.SharpPlanar.IntegerRoots.small_contains line 127
77. def OAI.SharpPlanar.IntegerRoots.poly32 line 129
78. lemma OAI.SharpPlanar.IntegerRoots.h32 line 130
79. def OAI.SharpPlanar.IntegerRoots.mul31 line 132
80. def OAI.SharpPlanar.IntegerRoots.poly31 line 133
81. lemma OAI.SharpPlanar.IntegerRoots.h31 line 134
82. def OAI.SharpPlanar.IntegerRoots.mul30 line 136
83. def OAI.SharpPlanar.IntegerRoots.poly30 line 137
84. lemma OAI.SharpPlanar.IntegerRoots.h30 line 138
85. def OAI.SharpPlanar.IntegerRoots.mul29 line 140
86. def OAI.SharpPlanar.IntegerRoots.poly29 line 141
87. lemma OAI.SharpPlanar.IntegerRoots.h29 line 142
88. def OAI.SharpPlanar.IntegerRoots.mul28 line 144
89. def OAI.SharpPlanar.IntegerRoots.poly28 line 145
90. lemma OAI.SharpPlanar.IntegerRoots.h28 line 146
91. def OAI.SharpPlanar.IntegerRoots.mul27 line 148
92. def OAI.SharpPlanar.IntegerRoots.poly27 line 149
93. lemma OAI.SharpPlanar.IntegerRoots.h27 line 150
94. def OAI.SharpPlanar.IntegerRoots.mul26 line 152
95. def OAI.SharpPlanar.IntegerRoots.poly26 line 153
96. lemma OAI.SharpPlanar.IntegerRoots.h26 line 154
97. def OAI.SharpPlanar.IntegerRoots.mul25 line 156
98. def OAI.SharpPlanar.IntegerRoots.poly25 line 157
99. lemma OAI.SharpPlanar.IntegerRoots.h25 line 158
100. def OAI.SharpPlanar.IntegerRoots.mul24 line 160
101. def OAI.SharpPlanar.IntegerRoots.poly24 line 161
102. lemma OAI.SharpPlanar.IntegerRoots.h24 line 162
103. def OAI.SharpPlanar.IntegerRoots.mul23 line 164
104. def OAI.SharpPlanar.IntegerRoots.poly23 line 165
105. lemma OAI.SharpPlanar.IntegerRoots.h23 line 166
106. def OAI.SharpPlanar.IntegerRoots.mul22 line 168
107. def OAI.SharpPlanar.IntegerRoots.poly22 line 169
108. lemma OAI.SharpPlanar.IntegerRoots.h22 line 170
109. def OAI.SharpPlanar.IntegerRoots.mul21 line 172
110. def OAI.SharpPlanar.IntegerRoots.poly21 line 173
111. lemma OAI.SharpPlanar.IntegerRoots.h21 line 174
112. def OAI.SharpPlanar.IntegerRoots.mul20 line 176
113. def OAI.SharpPlanar.IntegerRoots.poly20 line 177
114. lemma OAI.SharpPlanar.IntegerRoots.h20 line 178
115. def OAI.SharpPlanar.IntegerRoots.mul19 line 180
116. def OAI.SharpPlanar.IntegerRoots.poly19 line 181
117. lemma OAI.SharpPlanar.IntegerRoots.h19 line 182
118. def OAI.SharpPlanar.IntegerRoots.mul18 line 184
119. def OAI.SharpPlanar.IntegerRoots.poly18 line 185
120. lemma OAI.SharpPlanar.IntegerRoots.h18 line 186
121. def OAI.SharpPlanar.IntegerRoots.mul17 line 188
122. def OAI.SharpPlanar.IntegerRoots.poly17 line 189
123. lemma OAI.SharpPlanar.IntegerRoots.h17 line 190
124. def OAI.SharpPlanar.IntegerRoots.mul16 line 192
125. def OAI.SharpPlanar.IntegerRoots.poly16 line 193
126. lemma OAI.SharpPlanar.IntegerRoots.h16 line 194
127. def OAI.SharpPlanar.IntegerRoots.mul15 line 196
128. def OAI.SharpPlanar.IntegerRoots.poly15 line 197
129. lemma OAI.SharpPlanar.IntegerRoots.h15 line 198
130. def OAI.SharpPlanar.IntegerRoots.mul14 line 200
131. def OAI.SharpPlanar.IntegerRoots.poly14 line 201
132. lemma OAI.SharpPlanar.IntegerRoots.h14 line 202
133. def OAI.SharpPlanar.IntegerRoots.mul13 line 204
134. def OAI.SharpPlanar.IntegerRoots.poly13 line 205
135. lemma OAI.SharpPlanar.IntegerRoots.h13 line 206
136. def OAI.SharpPlanar.IntegerRoots.mul12 line 208
137. def OAI.SharpPlanar.IntegerRoots.poly12 line 209
138. lemma OAI.SharpPlanar.IntegerRoots.h12 line 210
139. def OAI.SharpPlanar.IntegerRoots.mul11 line 212
140. def OAI.SharpPlanar.IntegerRoots.poly11 line 213
141. lemma OAI.SharpPlanar.IntegerRoots.h11 line 214
142. def OAI.SharpPlanar.IntegerRoots.mul10 line 216
143. def OAI.SharpPlanar.IntegerRoots.poly10 line 217
144. lemma OAI.SharpPlanar.IntegerRoots.h10 line 218
145. def OAI.SharpPlanar.IntegerRoots.mul9 line 220
146. def OAI.SharpPlanar.IntegerRoots.poly9 line 221
147. lemma OAI.SharpPlanar.IntegerRoots.h9 line 222
148. def OAI.SharpPlanar.IntegerRoots.mul8 line 224
149. def OAI.SharpPlanar.IntegerRoots.poly8 line 225
150. lemma OAI.SharpPlanar.IntegerRoots.h8 line 226
151. def OAI.SharpPlanar.IntegerRoots.mul7 line 228
152. def OAI.SharpPlanar.IntegerRoots.poly7 line 229
153. lemma OAI.SharpPlanar.IntegerRoots.h7 line 230
154. def OAI.SharpPlanar.IntegerRoots.mul6 line 232
155. def OAI.SharpPlanar.IntegerRoots.poly6 line 233
156. lemma OAI.SharpPlanar.IntegerRoots.h6 line 234
157. def OAI.SharpPlanar.IntegerRoots.mul5 line 236
158. def OAI.SharpPlanar.IntegerRoots.poly5 line 237
159. lemma OAI.SharpPlanar.IntegerRoots.h5 line 238
160. def OAI.SharpPlanar.IntegerRoots.mul4 line 240
161. def OAI.SharpPlanar.IntegerRoots.poly4 line 241
162. lemma OAI.SharpPlanar.IntegerRoots.h4 line 242
163. def OAI.SharpPlanar.IntegerRoots.mul3 line 244
164. def OAI.SharpPlanar.IntegerRoots.poly3 line 245
165. lemma OAI.SharpPlanar.IntegerRoots.h3 line 246
166. def OAI.SharpPlanar.IntegerRoots.mul2 line 248
167. def OAI.SharpPlanar.IntegerRoots.poly2 line 249
168. lemma OAI.SharpPlanar.IntegerRoots.h2 line 250
169. def OAI.SharpPlanar.IntegerRoots.mul1 line 252
170. def OAI.SharpPlanar.IntegerRoots.poly1 line 253
171. lemma OAI.SharpPlanar.IntegerRoots.h1 line 254
172. def OAI.SharpPlanar.IntegerRoots.mul0 line 256
173. def OAI.SharpPlanar.IntegerRoots.poly0 line 257
174. lemma OAI.SharpPlanar.IntegerRoots.h0 line 258
175. def OAI.SharpPlanar.IntegerRoots.sq0 line 260
176. lemma OAI.SharpPlanar.IntegerRoots.sq0_contains line 261
177. def OAI.SharpPlanar.IntegerRoots.sq1 line 263
178. lemma OAI.SharpPlanar.IntegerRoots.sq1_contains line 264
179. def OAI.SharpPlanar.IntegerRoots.sq2 line 266
180. lemma OAI.SharpPlanar.IntegerRoots.sq2_contains line 267
181. def OAI.SharpPlanar.IntegerRoots.sq3 line 269
182. lemma OAI.SharpPlanar.IntegerRoots.sq3_contains line 270
183. def OAI.SharpPlanar.IntegerRoots.sq4 line 272
184. lemma OAI.SharpPlanar.IntegerRoots.sq4_contains line 273
185. def OAI.SharpPlanar.IntegerRoots.sq5 line 275
186. lemma OAI.SharpPlanar.IntegerRoots.sq5_contains line 276
187. def OAI.SharpPlanar.IntegerRoots.sq6 line 278
188. lemma OAI.SharpPlanar.IntegerRoots.sq6_contains line 279
189. def OAI.SharpPlanar.IntegerRoots.sq7 line 281
190. lemma OAI.SharpPlanar.IntegerRoots.sq7_contains line 282
191. def OAI.SharpPlanar.IntegerRoots.sq8 line 284
192. lemma OAI.SharpPlanar.IntegerRoots.sq8_contains line 285
193. def OAI.SharpPlanar.IntegerRoots.sq9 line 287
194. lemma OAI.SharpPlanar.IntegerRoots.sq9_contains line 288
195. def OAI.SharpPlanar.IntegerRoots.sq10 line 290
196. lemma OAI.SharpPlanar.IntegerRoots.sq10_contains line 291
197. def OAI.SharpPlanar.IntegerRoots.sq11 line 293
198. lemma OAI.SharpPlanar.IntegerRoots.sq11_contains line 294
199. lemma OAI.SharpPlanar.IntegerRoots.phase_contains line 296
200. def OAI.SharpPlanar.IntegerRoots.root0 line 304
201. lemma OAI.SharpPlanar.IntegerRoots.root0_contains line 305
202. def OAI.SharpPlanar.IntegerRoots.root1 line 307
203. lemma OAI.SharpPlanar.IntegerRoots.root1_contains line 308
204. def OAI.SharpPlanar.IntegerRoots.root2 line 309
205. lemma OAI.SharpPlanar.IntegerRoots.root2_contains line 310
206. def OAI.SharpPlanar.IntegerRoots.mid3 line 313
207. lemma OAI.SharpPlanar.IntegerRoots.mid3_contains line 314
208. def OAI.SharpPlanar.IntegerRoots.root3 line 315
209. lemma OAI.SharpPlanar.IntegerRoots.root3_contains line 316
210. def OAI.SharpPlanar.IntegerRoots.root4 line 319
211. lemma OAI.SharpPlanar.IntegerRoots.root4_contains line 320
212. def OAI.SharpPlanar.IntegerRoots.mid5 line 323
213. lemma OAI.SharpPlanar.IntegerRoots.mid5_contains line 324
214. def OAI.SharpPlanar.IntegerRoots.root5 line 325
215. lemma OAI.SharpPlanar.IntegerRoots.root5_contains line 326
216. def OAI.SharpPlanar.IntegerRoots.root6 line 329
217. lemma OAI.SharpPlanar.IntegerRoots.root6_contains line 330
218. def OAI.SharpPlanar.IntegerRoots.mid7 line 333
219. lemma OAI.SharpPlanar.IntegerRoots.mid7_contains line 334
220. def OAI.SharpPlanar.IntegerRoots.root7 line 335
221. lemma OAI.SharpPlanar.IntegerRoots.root7_contains line 336
222. def OAI.SharpPlanar.IntegerRoots.root8 line 339
223. lemma OAI.SharpPlanar.IntegerRoots.root8_contains line 340
224. def OAI.SharpPlanar.IntegerRoots.mid9 line 343
225. lemma OAI.SharpPlanar.IntegerRoots.mid9_contains line 344
226. def OAI.SharpPlanar.IntegerRoots.root9 line 345
227. lemma OAI.SharpPlanar.IntegerRoots.root9_contains line 346
228. def OAI.SharpPlanar.IntegerRoots.root10 line 349
229. lemma OAI.SharpPlanar.IntegerRoots.root10_contains line 350
230. def OAI.SharpPlanar.IntegerRoots.mid11 line 353
231. lemma OAI.SharpPlanar.IntegerRoots.mid11_contains line 354
232. def OAI.SharpPlanar.IntegerRoots.root11 line 355
233. lemma OAI.SharpPlanar.IntegerRoots.root11_contains line 356
234. def OAI.SharpPlanar.IntegerRoots.root12 line 359
235. lemma OAI.SharpPlanar.IntegerRoots.root12_contains line 360
236. def OAI.SharpPlanar.IntegerRoots.mid13 line 363
237. lemma OAI.SharpPlanar.IntegerRoots.mid13_contains line 364
238. def OAI.SharpPlanar.IntegerRoots.root13 line 365
239. lemma OAI.SharpPlanar.IntegerRoots.root13_contains line 366
240. def OAI.SharpPlanar.IntegerRoots.root14 line 369
241. lemma OAI.SharpPlanar.IntegerRoots.root14_contains line 370
242. def OAI.SharpPlanar.IntegerRoots.mid15 line 373
243. lemma OAI.SharpPlanar.IntegerRoots.mid15_contains line 374
244. def OAI.SharpPlanar.IntegerRoots.root15 line 375
245. lemma OAI.SharpPlanar.IntegerRoots.root15_contains line 376
246. def OAI.SharpPlanar.IntegerRoots.root16 line 379
247. lemma OAI.SharpPlanar.IntegerRoots.root16_contains line 380
248. def OAI.SharpPlanar.IntegerRoots.mid17 line 383
249. lemma OAI.SharpPlanar.IntegerRoots.mid17_contains line 384
250. def OAI.SharpPlanar.IntegerRoots.root17 line 385
251. lemma OAI.SharpPlanar.IntegerRoots.root17_contains line 386
252. def OAI.SharpPlanar.IntegerRoots.root18 line 389
253. lemma OAI.SharpPlanar.IntegerRoots.root18_contains line 390
254. def OAI.SharpPlanar.IntegerRoots.mid19 line 393
255. lemma OAI.SharpPlanar.IntegerRoots.mid19_contains line 394
256. def OAI.SharpPlanar.IntegerRoots.root19 line 395
257. lemma OAI.SharpPlanar.IntegerRoots.root19_contains line 396
258. def OAI.SharpPlanar.IntegerRoots.root20 line 399
259. lemma OAI.SharpPlanar.IntegerRoots.root20_contains line 400
260. def OAI.SharpPlanar.IntegerRoots.mid21 line 403
261. lemma OAI.SharpPlanar.IntegerRoots.mid21_contains line 404
262. def OAI.SharpPlanar.IntegerRoots.root21 line 405
263. lemma OAI.SharpPlanar.IntegerRoots.root21_contains line 406
264. def OAI.SharpPlanar.IntegerRoots.root22 line 409
265. lemma OAI.SharpPlanar.IntegerRoots.root22_contains line 410
266. def OAI.SharpPlanar.IntegerRoots.mid23 line 413
267. lemma OAI.SharpPlanar.IntegerRoots.mid23_contains line 414
268. def OAI.SharpPlanar.IntegerRoots.root23 line 415
269. lemma OAI.SharpPlanar.IntegerRoots.root23_contains line 416
270. def OAI.SharpPlanar.IntegerRoots.root24 line 419
271. lemma OAI.SharpPlanar.IntegerRoots.root24_contains line 420
272. def OAI.SharpPlanar.IntegerRoots.mid25 line 423
273. lemma OAI.SharpPlanar.IntegerRoots.mid25_contains line 424
274. def OAI.SharpPlanar.IntegerRoots.root25 line 425
275. lemma OAI.SharpPlanar.IntegerRoots.root25_contains line 426
276. def OAI.SharpPlanar.IntegerRoots.root26 line 429
277. lemma OAI.SharpPlanar.IntegerRoots.root26_contains line 430
278. def OAI.SharpPlanar.IntegerRoots.mid27 line 433
279. lemma OAI.SharpPlanar.IntegerRoots.mid27_contains line 434
280. def OAI.SharpPlanar.IntegerRoots.root27 line 435
281. lemma OAI.SharpPlanar.IntegerRoots.root27_contains line 436
282. def OAI.SharpPlanar.IntegerRoots.root28 line 439
283. lemma OAI.SharpPlanar.IntegerRoots.root28_contains line 440
284. def OAI.SharpPlanar.IntegerRoots.mid29 line 443
285. lemma OAI.SharpPlanar.IntegerRoots.mid29_contains line 444
286. def OAI.SharpPlanar.IntegerRoots.root29 line 445
287. lemma OAI.SharpPlanar.IntegerRoots.root29_contains line 446
288. def OAI.SharpPlanar.IntegerRoots.root30 line 449
289. lemma OAI.SharpPlanar.IntegerRoots.root30_contains line 450
290. def OAI.SharpPlanar.IntegerRoots.mid31 line 453
291. lemma OAI.SharpPlanar.IntegerRoots.mid31_contains line 454
292. def OAI.SharpPlanar.IntegerRoots.root31 line 455
293. lemma OAI.SharpPlanar.IntegerRoots.root31_contains line 456
294. def OAI.SharpPlanar.IntegerRoots.root32 line 459
295. lemma OAI.SharpPlanar.IntegerRoots.root32_contains line 460
296. def OAI.SharpPlanar.IntegerRoots.mid33 line 463
297. lemma OAI.SharpPlanar.IntegerRoots.mid33_contains line 464
298. def OAI.SharpPlanar.IntegerRoots.root33 line 465
299. lemma OAI.SharpPlanar.IntegerRoots.root33_contains line 466
300. def OAI.SharpPlanar.IntegerRoots.root34 line 469
301. lemma OAI.SharpPlanar.IntegerRoots.root34_contains line 470
302. def OAI.SharpPlanar.IntegerRoots.mid35 line 473
303. lemma OAI.SharpPlanar.IntegerRoots.mid35_contains line 474
304. def OAI.SharpPlanar.IntegerRoots.root35 line 475
305. lemma OAI.SharpPlanar.IntegerRoots.root35_contains line 476
306. def OAI.SharpPlanar.IntegerRoots.root36 line 479
307. lemma OAI.SharpPlanar.IntegerRoots.root36_contains line 480
308. def OAI.SharpPlanar.IntegerRoots.mid37 line 483
309. lemma OAI.SharpPlanar.IntegerRoots.mid37_contains line 484
310. def OAI.SharpPlanar.IntegerRoots.root37 line 485
311. lemma OAI.SharpPlanar.IntegerRoots.root37_contains line 486
312. def OAI.SharpPlanar.IntegerRoots.root38 line 489
313. lemma OAI.SharpPlanar.IntegerRoots.root38_contains line 490
314. def OAI.SharpPlanar.IntegerRoots.mid39 line 493
315. lemma OAI.SharpPlanar.IntegerRoots.mid39_contains line 494
316. def OAI.SharpPlanar.IntegerRoots.root39 line 495
317. lemma OAI.SharpPlanar.IntegerRoots.root39_contains line 496
318. def OAI.SharpPlanar.IntegerRoots.root40 line 499
319. lemma OAI.SharpPlanar.IntegerRoots.root40_contains line 500
320. def OAI.SharpPlanar.IntegerRoots.mid41 line 503
321. lemma OAI.SharpPlanar.IntegerRoots.mid41_contains line 504
322. def OAI.SharpPlanar.IntegerRoots.root41 line 505
323. lemma OAI.SharpPlanar.IntegerRoots.root41_contains line 506
324. def OAI.SharpPlanar.IntegerRoots.root42 line 509
325. lemma OAI.SharpPlanar.IntegerRoots.root42_contains line 510
326. def OAI.SharpPlanar.IntegerRoots.mid43 line 513
327. lemma OAI.SharpPlanar.IntegerRoots.mid43_contains line 514
328. def OAI.SharpPlanar.IntegerRoots.root43 line 515
329. lemma OAI.SharpPlanar.IntegerRoots.root43_contains line 516
330. def OAI.SharpPlanar.IntegerRoots.root44 line 519
331. lemma OAI.SharpPlanar.IntegerRoots.root44_contains line 520
332. def OAI.SharpPlanar.IntegerRoots.mid45 line 523
333. lemma OAI.SharpPlanar.IntegerRoots.mid45_contains line 524
334. def OAI.SharpPlanar.IntegerRoots.root45 line 525
335. lemma OAI.SharpPlanar.IntegerRoots.root45_contains line 526
336. def OAI.SharpPlanar.IntegerRoots.root46 line 529
337. lemma OAI.SharpPlanar.IntegerRoots.root46_contains line 530
338. def OAI.SharpPlanar.IntegerRoots.mid47 line 533
339. lemma OAI.SharpPlanar.IntegerRoots.mid47_contains line 534
340. def OAI.SharpPlanar.IntegerRoots.root47 line 535
341. lemma OAI.SharpPlanar.IntegerRoots.root47_contains line 536
342. def OAI.SharpPlanar.IntegerRoots.root48 line 539
343. lemma OAI.SharpPlanar.IntegerRoots.root48_contains line 540
344. def OAI.SharpPlanar.IntegerRoots.mid49 line 543
345. lemma OAI.SharpPlanar.IntegerRoots.mid49_contains line 544
346. def OAI.SharpPlanar.IntegerRoots.root49 line 545
347. lemma OAI.SharpPlanar.IntegerRoots.root49_contains line 546
348. def OAI.SharpPlanar.IntegerRoots.root50 line 549
349. lemma OAI.SharpPlanar.IntegerRoots.root50_contains line 550
350. def OAI.SharpPlanar.IntegerRoots.mid51 line 553
351. lemma OAI.SharpPlanar.IntegerRoots.mid51_contains line 554
352. def OAI.SharpPlanar.IntegerRoots.root51 line 555
353. lemma OAI.SharpPlanar.IntegerRoots.root51_contains line 556
354. def OAI.SharpPlanar.IntegerRoots.root52 line 559
355. lemma OAI.SharpPlanar.IntegerRoots.root52_contains line 560
356. def OAI.SharpPlanar.IntegerRoots.mid53 line 563
357. lemma OAI.SharpPlanar.IntegerRoots.mid53_contains line 564
358. def OAI.SharpPlanar.IntegerRoots.root53 line 565
359. lemma OAI.SharpPlanar.IntegerRoots.root53_contains line 566
360. def OAI.SharpPlanar.IntegerRoots.root54 line 569
361. lemma OAI.SharpPlanar.IntegerRoots.root54_contains line 570
362. def OAI.SharpPlanar.IntegerRoots.mid55 line 573
363. lemma OAI.SharpPlanar.IntegerRoots.mid55_contains line 574
364. def OAI.SharpPlanar.IntegerRoots.root55 line 575
365. lemma OAI.SharpPlanar.IntegerRoots.root55_contains line 576
366. def OAI.SharpPlanar.IntegerRoots.root56 line 579
367. lemma OAI.SharpPlanar.IntegerRoots.root56_contains line 580
368. def OAI.SharpPlanar.IntegerRoots.mid57 line 583
369. lemma OAI.SharpPlanar.IntegerRoots.mid57_contains line 584
370. def OAI.SharpPlanar.IntegerRoots.root57 line 585
371. lemma OAI.SharpPlanar.IntegerRoots.root57_contains line 586
372. def OAI.SharpPlanar.IntegerRoots.root58 line 589
373. lemma OAI.SharpPlanar.IntegerRoots.root58_contains line 590
374. def OAI.SharpPlanar.IntegerRoots.mid59 line 593
375. lemma OAI.SharpPlanar.IntegerRoots.mid59_contains line 594
376. def OAI.SharpPlanar.IntegerRoots.root59 line 595
377. lemma OAI.SharpPlanar.IntegerRoots.root59_contains line 596
378. def OAI.SharpPlanar.IntegerRoots.root60 line 599
379. lemma OAI.SharpPlanar.IntegerRoots.root60_contains line 600
380. def OAI.SharpPlanar.IntegerRoots.mid61 line 603
381. lemma OAI.SharpPlanar.IntegerRoots.mid61_contains line 604
382. def OAI.SharpPlanar.IntegerRoots.root61 line 605
383. lemma OAI.SharpPlanar.IntegerRoots.root61_contains line 606
384. def OAI.SharpPlanar.IntegerRoots.root62 line 609
385. lemma OAI.SharpPlanar.IntegerRoots.root62_contains line 610
386. def OAI.SharpPlanar.IntegerRoots.mid63 line 613
387. lemma OAI.SharpPlanar.IntegerRoots.mid63_contains line 614
388. def OAI.SharpPlanar.IntegerRoots.root63 line 615
389. lemma OAI.SharpPlanar.IntegerRoots.root63_contains line 616
390. def OAI.SharpPlanar.IntegerRoots.root64 line 619
391. lemma OAI.SharpPlanar.IntegerRoots.root64_contains line 620
392. def OAI.SharpPlanar.IntegerRoots.mid65 line 623
393. lemma OAI.SharpPlanar.IntegerRoots.mid65_contains line 624
394. def OAI.SharpPlanar.IntegerRoots.root65 line 625
395. lemma OAI.SharpPlanar.IntegerRoots.root65_contains line 626
396. def OAI.SharpPlanar.IntegerRoots.root66 line 629
397. lemma OAI.SharpPlanar.IntegerRoots.root66_contains line 630
398. def OAI.SharpPlanar.IntegerRoots.mid67 line 633
399. lemma OAI.SharpPlanar.IntegerRoots.mid67_contains line 634
400. def OAI.SharpPlanar.IntegerRoots.root67 line 635
401. lemma OAI.SharpPlanar.IntegerRoots.root67_contains line 636
402. def OAI.SharpPlanar.IntegerRoots.root68 line 639
403. lemma OAI.SharpPlanar.IntegerRoots.root68_contains line 640
404. def OAI.SharpPlanar.IntegerRoots.mid69 line 643
405. lemma OAI.SharpPlanar.IntegerRoots.mid69_contains line 644
406. def OAI.SharpPlanar.IntegerRoots.root69 line 645
407. lemma OAI.SharpPlanar.IntegerRoots.root69_contains line 646
408. def OAI.SharpPlanar.IntegerRoots.root70 line 649
409. lemma OAI.SharpPlanar.IntegerRoots.root70_contains line 650
410. def OAI.SharpPlanar.IntegerRoots.mid71 line 653
411. lemma OAI.SharpPlanar.IntegerRoots.mid71_contains line 654
412. def OAI.SharpPlanar.IntegerRoots.root71 line 655
413. lemma OAI.SharpPlanar.IntegerRoots.root71_contains line 656
414. def OAI.SharpPlanar.IntegerRoots.root72 line 659
415. lemma OAI.SharpPlanar.IntegerRoots.root72_contains line 660
416. def OAI.SharpPlanar.IntegerRoots.mid73 line 663
417. lemma OAI.SharpPlanar.IntegerRoots.mid73_contains line 664
418. def OAI.SharpPlanar.IntegerRoots.root73 line 665
419. lemma OAI.SharpPlanar.IntegerRoots.root73_contains line 666
420. def OAI.SharpPlanar.IntegerRoots.root74 line 669
421. lemma OAI.SharpPlanar.IntegerRoots.root74_contains line 670
422. def OAI.SharpPlanar.IntegerRoots.mid75 line 673
423. lemma OAI.SharpPlanar.IntegerRoots.mid75_contains line 674
424. def OAI.SharpPlanar.IntegerRoots.root75 line 675
425. lemma OAI.SharpPlanar.IntegerRoots.root75_contains line 676
426. def OAI.SharpPlanar.IntegerRoots.root76 line 679
427. lemma OAI.SharpPlanar.IntegerRoots.root76_contains line 680
428. def OAI.SharpPlanar.IntegerRoots.mid77 line 683
429. lemma OAI.SharpPlanar.IntegerRoots.mid77_contains line 684
430. def OAI.SharpPlanar.IntegerRoots.root77 line 685
431. lemma OAI.SharpPlanar.IntegerRoots.root77_contains line 686
432. def OAI.SharpPlanar.IntegerRoots.root78 line 689
433. lemma OAI.SharpPlanar.IntegerRoots.root78_contains line 690
434. def OAI.SharpPlanar.IntegerRoots.mid79 line 693
435. lemma OAI.SharpPlanar.IntegerRoots.mid79_contains line 694
436. def OAI.SharpPlanar.IntegerRoots.root79 line 695
437. lemma OAI.SharpPlanar.IntegerRoots.root79_contains line 696
438. def OAI.SharpPlanar.IntegerRoots.root80 line 699
439. lemma OAI.SharpPlanar.IntegerRoots.root80_contains line 700
440. def OAI.SharpPlanar.IntegerRoots.mid81 line 703
441. lemma OAI.SharpPlanar.IntegerRoots.mid81_contains line 704
442. def OAI.SharpPlanar.IntegerRoots.root81 line 705
443. lemma OAI.SharpPlanar.IntegerRoots.root81_contains line 706
444. def OAI.SharpPlanar.IntegerRoots.root82 line 709
445. lemma OAI.SharpPlanar.IntegerRoots.root82_contains line 710
446. def OAI.SharpPlanar.IntegerRoots.mid83 line 713
447. lemma OAI.SharpPlanar.IntegerRoots.mid83_contains line 714
448. def OAI.SharpPlanar.IntegerRoots.root83 line 715
449. lemma OAI.SharpPlanar.IntegerRoots.root83_contains line 716
450. def OAI.SharpPlanar.IntegerRoots.root84 line 719
451. lemma OAI.SharpPlanar.IntegerRoots.root84_contains line 720
452. def OAI.SharpPlanar.IntegerRoots.mid85 line 723
453. lemma OAI.SharpPlanar.IntegerRoots.mid85_contains line 724
454. def OAI.SharpPlanar.IntegerRoots.root85 line 725
455. lemma OAI.SharpPlanar.IntegerRoots.root85_contains line 726
456. def OAI.SharpPlanar.IntegerRoots.root86 line 729
457. lemma OAI.SharpPlanar.IntegerRoots.root86_contains line 730
458. def OAI.SharpPlanar.IntegerRoots.mid87 line 733
459. lemma OAI.SharpPlanar.IntegerRoots.mid87_contains line 734
460. def OAI.SharpPlanar.IntegerRoots.root87 line 735
461. lemma OAI.SharpPlanar.IntegerRoots.root87_contains line 736
462. def OAI.SharpPlanar.IntegerRoots.root88 line 739
463. lemma OAI.SharpPlanar.IntegerRoots.root88_contains line 740
464. def OAI.SharpPlanar.IntegerRoots.mid89 line 743
465. lemma OAI.SharpPlanar.IntegerRoots.mid89_contains line 744
466. def OAI.SharpPlanar.IntegerRoots.root89 line 745
467. lemma OAI.SharpPlanar.IntegerRoots.root89_contains line 746
468. def OAI.SharpPlanar.IntegerRoots.root90 line 749
469. lemma OAI.SharpPlanar.IntegerRoots.root90_contains line 750
470. def OAI.SharpPlanar.IntegerRoots.mid91 line 753
471. lemma OAI.SharpPlanar.IntegerRoots.mid91_contains line 754
472. def OAI.SharpPlanar.IntegerRoots.root91 line 755
473. lemma OAI.SharpPlanar.IntegerRoots.root91_contains line 756
474. def OAI.SharpPlanar.IntegerRoots.root92 line 759
475. lemma OAI.SharpPlanar.IntegerRoots.root92_contains line 760
476. def OAI.SharpPlanar.IntegerRoots.mid93 line 763
477. lemma OAI.SharpPlanar.IntegerRoots.mid93_contains line 764
478. def OAI.SharpPlanar.IntegerRoots.root93 line 765
479. lemma OAI.SharpPlanar.IntegerRoots.root93_contains line 766
480. def OAI.SharpPlanar.IntegerRoots.root94 line 769
481. lemma OAI.SharpPlanar.IntegerRoots.root94_contains line 770
482. def OAI.SharpPlanar.IntegerRoots.mid95 line 773
483. lemma OAI.SharpPlanar.IntegerRoots.mid95_contains line 774
484. def OAI.SharpPlanar.IntegerRoots.root95 line 775
485. lemma OAI.SharpPlanar.IntegerRoots.root95_contains line 776
486. def OAI.SharpPlanar.IntegerRoots.root96 line 779
487. lemma OAI.SharpPlanar.IntegerRoots.root96_contains line 780
488. def OAI.SharpPlanar.IntegerRoots.mid97 line 783
489. lemma OAI.SharpPlanar.IntegerRoots.mid97_contains line 784
490. def OAI.SharpPlanar.IntegerRoots.root97 line 785
491. lemma OAI.SharpPlanar.IntegerRoots.root97_contains line 786
492. def OAI.SharpPlanar.IntegerRoots.root98 line 789
493. lemma OAI.SharpPlanar.IntegerRoots.root98_contains line 790
494. def OAI.SharpPlanar.IntegerRoots.mid99 line 793
495. lemma OAI.SharpPlanar.IntegerRoots.mid99_contains line 794
496. def OAI.SharpPlanar.IntegerRoots.root99 line 795
497. lemma OAI.SharpPlanar.IntegerRoots.root99_contains line 796
498. def OAI.SharpPlanar.IntegerRoots.root100 line 799
499. lemma OAI.SharpPlanar.IntegerRoots.root100_contains line 800
500. def OAI.SharpPlanar.IntegerRoots.mid101 line 803
501. lemma OAI.SharpPlanar.IntegerRoots.mid101_contains line 804
502. def OAI.SharpPlanar.IntegerRoots.root101 line 805
503. lemma OAI.SharpPlanar.IntegerRoots.root101_contains line 806
504. def OAI.SharpPlanar.IntegerRoots.root102 line 809
505. lemma OAI.SharpPlanar.IntegerRoots.root102_contains line 810
506. def OAI.SharpPlanar.IntegerRoots.mid103 line 813
507. lemma OAI.SharpPlanar.IntegerRoots.mid103_contains line 814
508. def OAI.SharpPlanar.IntegerRoots.root103 line 815
509. lemma OAI.SharpPlanar.IntegerRoots.root103_contains line 816
510. def OAI.SharpPlanar.IntegerRoots.root104 line 819
511. lemma OAI.SharpPlanar.IntegerRoots.root104_contains line 820
512. def OAI.SharpPlanar.IntegerRoots.mid105 line 823
513. lemma OAI.SharpPlanar.IntegerRoots.mid105_contains line 824
514. def OAI.SharpPlanar.IntegerRoots.root105 line 825
515. lemma OAI.SharpPlanar.IntegerRoots.root105_contains line 826
516. def OAI.SharpPlanar.IntegerRoots.root106 line 829
517. lemma OAI.SharpPlanar.IntegerRoots.root106_contains line 830
518. def OAI.SharpPlanar.IntegerRoots.mid107 line 833
519. lemma OAI.SharpPlanar.IntegerRoots.mid107_contains line 834
520. def OAI.SharpPlanar.IntegerRoots.root107 line 835
521. lemma OAI.SharpPlanar.IntegerRoots.root107_contains line 836
522. def OAI.SharpPlanar.IntegerRoots.root108 line 839
523. lemma OAI.SharpPlanar.IntegerRoots.root108_contains line 840
524. def OAI.SharpPlanar.IntegerRoots.mid109 line 843
525. lemma OAI.SharpPlanar.IntegerRoots.mid109_contains line 844
526. def OAI.SharpPlanar.IntegerRoots.root109 line 845
527. lemma OAI.SharpPlanar.IntegerRoots.root109_contains line 846
528. def OAI.SharpPlanar.IntegerRoots.root110 line 849
529. lemma OAI.SharpPlanar.IntegerRoots.root110_contains line 850
530. def OAI.SharpPlanar.IntegerRoots.mid111 line 853
531. lemma OAI.SharpPlanar.IntegerRoots.mid111_contains line 854
532. def OAI.SharpPlanar.IntegerRoots.root111 line 855
533. lemma OAI.SharpPlanar.IntegerRoots.root111_contains line 856
534. def OAI.SharpPlanar.IntegerRoots.root112 line 859
535. lemma OAI.SharpPlanar.IntegerRoots.root112_contains line 860
536. def OAI.SharpPlanar.IntegerRoots.mid113 line 863
537. lemma OAI.SharpPlanar.IntegerRoots.mid113_contains line 864
538. def OAI.SharpPlanar.IntegerRoots.root113 line 865
539. lemma OAI.SharpPlanar.IntegerRoots.root113_contains line 866
540. def OAI.SharpPlanar.IntegerRoots.root114 line 869
541. lemma OAI.SharpPlanar.IntegerRoots.root114_contains line 870
542. def OAI.SharpPlanar.IntegerRoots.mid115 line 873
543. lemma OAI.SharpPlanar.IntegerRoots.mid115_contains line 874
544. def OAI.SharpPlanar.IntegerRoots.root115 line 875
545. lemma OAI.SharpPlanar.IntegerRoots.root115_contains line 876
546. def OAI.SharpPlanar.IntegerRoots.root116 line 879
547. lemma OAI.SharpPlanar.IntegerRoots.root116_contains line 880
548. def OAI.SharpPlanar.IntegerRoots.mid117 line 883
549. lemma OAI.SharpPlanar.IntegerRoots.mid117_contains line 884
550. def OAI.SharpPlanar.IntegerRoots.root117 line 885
551. lemma OAI.SharpPlanar.IntegerRoots.root117_contains line 886
552. def OAI.SharpPlanar.IntegerRoots.root118 line 889
553. lemma OAI.SharpPlanar.IntegerRoots.root118_contains line 890
554. def OAI.SharpPlanar.IntegerRoots.mid119 line 893
555. lemma OAI.SharpPlanar.IntegerRoots.mid119_contains line 894
556. def OAI.SharpPlanar.IntegerRoots.root119 line 895
557. lemma OAI.SharpPlanar.IntegerRoots.root119_contains line 896
558. def OAI.SharpPlanar.IntegerRoots.root120 line 899
559. lemma OAI.SharpPlanar.IntegerRoots.root120_contains line 900
560. def OAI.SharpPlanar.IntegerRoots.mid121 line 903
561. lemma OAI.SharpPlanar.IntegerRoots.mid121_contains line 904
562. def OAI.SharpPlanar.IntegerRoots.root121 line 905
563. lemma OAI.SharpPlanar.IntegerRoots.root121_contains line 906
564. def OAI.SharpPlanar.IntegerRoots.root122 line 909
565. lemma OAI.SharpPlanar.IntegerRoots.root122_contains line 910
566. def OAI.SharpPlanar.IntegerRoots.mid123 line 913
567. lemma OAI.SharpPlanar.IntegerRoots.mid123_contains line 914
568. def OAI.SharpPlanar.IntegerRoots.root123 line 915
569. lemma OAI.SharpPlanar.IntegerRoots.root123_contains line 916
570. def OAI.SharpPlanar.IntegerRoots.root124 line 919
571. lemma OAI.SharpPlanar.IntegerRoots.root124_contains line 920
572. def OAI.SharpPlanar.IntegerRoots.mid125 line 923
573. lemma OAI.SharpPlanar.IntegerRoots.mid125_contains line 924
574. def OAI.SharpPlanar.IntegerRoots.root125 line 925
575. lemma OAI.SharpPlanar.IntegerRoots.root125_contains line 926
576. def OAI.SharpPlanar.IntegerRoots.root126 line 929
577. lemma OAI.SharpPlanar.IntegerRoots.root126_contains line 930
578. def OAI.SharpPlanar.IntegerRoots.mid127 line 933
579. lemma OAI.SharpPlanar.IntegerRoots.mid127_contains line 934
580. def OAI.SharpPlanar.IntegerRoots.root127 line 935
581. lemma OAI.SharpPlanar.IntegerRoots.root127_contains line 936
582. def OAI.SharpPlanar.IntegerRoots.root128 line 939
583. lemma OAI.SharpPlanar.IntegerRoots.root128_contains line 940
584. def OAI.SharpPlanar.IntegerRoots.mid129 line 943
585. lemma OAI.SharpPlanar.IntegerRoots.mid129_contains line 944
586. def OAI.SharpPlanar.IntegerRoots.root129 line 945
587. lemma OAI.SharpPlanar.IntegerRoots.root129_contains line 946
588. def OAI.SharpPlanar.IntegerRoots.root130 line 949
589. lemma OAI.SharpPlanar.IntegerRoots.root130_contains line 950
590. def OAI.SharpPlanar.IntegerRoots.mid131 line 953
591. lemma OAI.SharpPlanar.IntegerRoots.mid131_contains line 954
592. def OAI.SharpPlanar.IntegerRoots.root131 line 955
593. lemma OAI.SharpPlanar.IntegerRoots.root131_contains line 956
594. def OAI.SharpPlanar.IntegerRoots.root132 line 959
595. lemma OAI.SharpPlanar.IntegerRoots.root132_contains line 960
596. def OAI.SharpPlanar.IntegerRoots.mid133 line 963
597. lemma OAI.SharpPlanar.IntegerRoots.mid133_contains line 964
598. def OAI.SharpPlanar.IntegerRoots.root133 line 965
599. lemma OAI.SharpPlanar.IntegerRoots.root133_contains line 966
600. def OAI.SharpPlanar.IntegerRoots.root134 line 969
601. lemma OAI.SharpPlanar.IntegerRoots.root134_contains line 970
602. def OAI.SharpPlanar.IntegerRoots.mid135 line 973
603. lemma OAI.SharpPlanar.IntegerRoots.mid135_contains line 974
604. def OAI.SharpPlanar.IntegerRoots.root135 line 975
605. lemma OAI.SharpPlanar.IntegerRoots.root135_contains line 976
606. def OAI.SharpPlanar.IntegerRoots.root136 line 979
607. lemma OAI.SharpPlanar.IntegerRoots.root136_contains line 980
608. def OAI.SharpPlanar.IntegerRoots.mid137 line 983
609. lemma OAI.SharpPlanar.IntegerRoots.mid137_contains line 984
610. def OAI.SharpPlanar.IntegerRoots.root137 line 985
611. lemma OAI.SharpPlanar.IntegerRoots.root137_contains line 986
612. def OAI.SharpPlanar.IntegerRoots.root138 line 989
613. lemma OAI.SharpPlanar.IntegerRoots.root138_contains line 990
614. def OAI.SharpPlanar.IntegerRoots.mid139 line 993
615. lemma OAI.SharpPlanar.IntegerRoots.mid139_contains line 994
616. def OAI.SharpPlanar.IntegerRoots.root139 line 995
617. lemma OAI.SharpPlanar.IntegerRoots.root139_contains line 996
618. def OAI.SharpPlanar.IntegerRoots.root140 line 999
619. lemma OAI.SharpPlanar.IntegerRoots.root140_contains line 1000
620. def OAI.SharpPlanar.IntegerRoots.mid141 line 1003
621. lemma OAI.SharpPlanar.IntegerRoots.mid141_contains line 1004
622. def OAI.SharpPlanar.IntegerRoots.root141 line 1005
623. lemma OAI.SharpPlanar.IntegerRoots.root141_contains line 1006
624. def OAI.SharpPlanar.IntegerRoots.root142 line 1009
625. lemma OAI.SharpPlanar.IntegerRoots.root142_contains line 1010
626. def OAI.SharpPlanar.IntegerRoots.mid143 line 1013
627. lemma OAI.SharpPlanar.IntegerRoots.mid143_contains line 1014
628. def OAI.SharpPlanar.IntegerRoots.root143 line 1015
629. lemma OAI.SharpPlanar.IntegerRoots.root143_contains line 1016
630. def OAI.SharpPlanar.IntegerRoots.root144 line 1019
631. lemma OAI.SharpPlanar.IntegerRoots.root144_contains line 1020
632. def OAI.SharpPlanar.IntegerRoots.mid145 line 1023
633. lemma OAI.SharpPlanar.IntegerRoots.mid145_contains line 1024
634. def OAI.SharpPlanar.IntegerRoots.root145 line 1025
635. lemma OAI.SharpPlanar.IntegerRoots.root145_contains line 1026
636. def OAI.SharpPlanar.IntegerRoots.root146 line 1029
637. lemma OAI.SharpPlanar.IntegerRoots.root146_contains line 1030
638. def OAI.SharpPlanar.IntegerRoots.mid147 line 1033
639. lemma OAI.SharpPlanar.IntegerRoots.mid147_contains line 1034
640. def OAI.SharpPlanar.IntegerRoots.root147 line 1035
641. lemma OAI.SharpPlanar.IntegerRoots.root147_contains line 1036
642. def OAI.SharpPlanar.IntegerRoots.root148 line 1039
643. lemma OAI.SharpPlanar.IntegerRoots.root148_contains line 1040
644. def OAI.SharpPlanar.IntegerRoots.mid149 line 1043
645. lemma OAI.SharpPlanar.IntegerRoots.mid149_contains line 1044
646. def OAI.SharpPlanar.IntegerRoots.root149 line 1045
647. lemma OAI.SharpPlanar.IntegerRoots.root149_contains line 1046
648. def OAI.SharpPlanar.IntegerRoots.root150 line 1049
649. lemma OAI.SharpPlanar.IntegerRoots.root150_contains line 1050
650. def OAI.SharpPlanar.IntegerRoots.mid151 line 1053
651. lemma OAI.SharpPlanar.IntegerRoots.mid151_contains line 1054
652. def OAI.SharpPlanar.IntegerRoots.root151 line 1055
653. lemma OAI.SharpPlanar.IntegerRoots.root151_contains line 1056
654. def OAI.SharpPlanar.IntegerRoots.root152 line 1059
655. lemma OAI.SharpPlanar.IntegerRoots.root152_contains line 1060
656. def OAI.SharpPlanar.IntegerRoots.mid153 line 1063
657. lemma OAI.SharpPlanar.IntegerRoots.mid153_contains line 1064
658. def OAI.SharpPlanar.IntegerRoots.root153 line 1065
659. lemma OAI.SharpPlanar.IntegerRoots.root153_contains line 1066
660. def OAI.SharpPlanar.IntegerRoots.root154 line 1069
661. lemma OAI.SharpPlanar.IntegerRoots.root154_contains line 1070
662. def OAI.SharpPlanar.IntegerRoots.mid155 line 1073
663. lemma OAI.SharpPlanar.IntegerRoots.mid155_contains line 1074
664. def OAI.SharpPlanar.IntegerRoots.root155 line 1075
665. lemma OAI.SharpPlanar.IntegerRoots.root155_contains line 1076
666. def OAI.SharpPlanar.IntegerRoots.root156 line 1079
667. lemma OAI.SharpPlanar.IntegerRoots.root156_contains line 1080
668. def OAI.SharpPlanar.IntegerRoots.mid157 line 1083
669. lemma OAI.SharpPlanar.IntegerRoots.mid157_contains line 1084
670. def OAI.SharpPlanar.IntegerRoots.root157 line 1085
671. lemma OAI.SharpPlanar.IntegerRoots.root157_contains line 1086
672. def OAI.SharpPlanar.IntegerRoots.root158 line 1089
673. lemma OAI.SharpPlanar.IntegerRoots.root158_contains line 1090
674. def OAI.SharpPlanar.IntegerRoots.mid159 line 1093
675. lemma OAI.SharpPlanar.IntegerRoots.mid159_contains line 1094
676. def OAI.SharpPlanar.IntegerRoots.root159 line 1095
677. lemma OAI.SharpPlanar.IntegerRoots.root159_contains line 1096
678. def OAI.SharpPlanar.IntegerRoots.root160 line 1099
679. lemma OAI.SharpPlanar.IntegerRoots.root160_contains line 1100
680. def OAI.SharpPlanar.IntegerRoots.mid161 line 1103
681. lemma OAI.SharpPlanar.IntegerRoots.mid161_contains line 1104
682. def OAI.SharpPlanar.IntegerRoots.root161 line 1105
683. lemma OAI.SharpPlanar.IntegerRoots.root161_contains line 1106
684. def OAI.SharpPlanar.IntegerRoots.root162 line 1109
685. lemma OAI.SharpPlanar.IntegerRoots.root162_contains line 1110
686. def OAI.SharpPlanar.IntegerRoots.mid163 line 1113
687. lemma OAI.SharpPlanar.IntegerRoots.mid163_contains line 1114
688. def OAI.SharpPlanar.IntegerRoots.root163 line 1115
689. lemma OAI.SharpPlanar.IntegerRoots.root163_contains line 1116
690. def OAI.SharpPlanar.IntegerRoots.root164 line 1119
691. lemma OAI.SharpPlanar.IntegerRoots.root164_contains line 1120
692. def OAI.SharpPlanar.IntegerRoots.mid165 line 1123
693. lemma OAI.SharpPlanar.IntegerRoots.mid165_contains line 1124
694. def OAI.SharpPlanar.IntegerRoots.root165 line 1125
695. lemma OAI.SharpPlanar.IntegerRoots.root165_contains line 1126
696. def OAI.SharpPlanar.IntegerRoots.root166 line 1129
697. lemma OAI.SharpPlanar.IntegerRoots.root166_contains line 1130
698. def OAI.SharpPlanar.IntegerRoots.mid167 line 1133
699. lemma OAI.SharpPlanar.IntegerRoots.mid167_contains line 1134
700. def OAI.SharpPlanar.IntegerRoots.root167 line 1135
701. lemma OAI.SharpPlanar.IntegerRoots.root167_contains line 1136
702. def OAI.SharpPlanar.IntegerRoots.root168 line 1139
703. lemma OAI.SharpPlanar.IntegerRoots.root168_contains line 1140
704. def OAI.SharpPlanar.IntegerRoots.mid169 line 1143
705. lemma OAI.SharpPlanar.IntegerRoots.mid169_contains line 1144
706. def OAI.SharpPlanar.IntegerRoots.root169 line 1145
707. lemma OAI.SharpPlanar.IntegerRoots.root169_contains line 1146
708. def OAI.SharpPlanar.IntegerRoots.root170 line 1149
709. lemma OAI.SharpPlanar.IntegerRoots.root170_contains line 1150
710. def OAI.SharpPlanar.IntegerRoots.mid171 line 1153
711. lemma OAI.SharpPlanar.IntegerRoots.mid171_contains line 1154
712. def OAI.SharpPlanar.IntegerRoots.root171 line 1155
713. lemma OAI.SharpPlanar.IntegerRoots.root171_contains line 1156
714. def OAI.SharpPlanar.IntegerRoots.root172 line 1159
715. lemma OAI.SharpPlanar.IntegerRoots.root172_contains line 1160
716. def OAI.SharpPlanar.IntegerRoots.mid173 line 1163
717. lemma OAI.SharpPlanar.IntegerRoots.mid173_contains line 1164
718. def OAI.SharpPlanar.IntegerRoots.root173 line 1165
719. lemma OAI.SharpPlanar.IntegerRoots.root173_contains line 1166
720. def OAI.SharpPlanar.IntegerRoots.root174 line 1169
721. lemma OAI.SharpPlanar.IntegerRoots.root174_contains line 1170
722. def OAI.SharpPlanar.IntegerRoots.mid175 line 1173
723. lemma OAI.SharpPlanar.IntegerRoots.mid175_contains line 1174
724. def OAI.SharpPlanar.IntegerRoots.root175 line 1175
725. lemma OAI.SharpPlanar.IntegerRoots.root175_contains line 1176
726. def OAI.SharpPlanar.IntegerRoots.root176 line 1179
727. lemma OAI.SharpPlanar.IntegerRoots.root176_contains line 1180
728. def OAI.SharpPlanar.IntegerRoots.mid177 line 1183
729. lemma OAI.SharpPlanar.IntegerRoots.mid177_contains line 1184
730. def OAI.SharpPlanar.IntegerRoots.root177 line 1185
731. lemma OAI.SharpPlanar.IntegerRoots.root177_contains line 1186
732. def OAI.SharpPlanar.IntegerRoots.root178 line 1189
733. lemma OAI.SharpPlanar.IntegerRoots.root178_contains line 1190
734. def OAI.SharpPlanar.IntegerRoots.mid179 line 1193
735. lemma OAI.SharpPlanar.IntegerRoots.mid179_contains line 1194
736. def OAI.SharpPlanar.IntegerRoots.root179 line 1195
737. lemma OAI.SharpPlanar.IntegerRoots.root179_contains line 1196
738. def OAI.SharpPlanar.IntegerRoots.root180 line 1199
739. lemma OAI.SharpPlanar.IntegerRoots.root180_contains line 1200
740. def OAI.SharpPlanar.IntegerRoots.mid181 line 1203
741. lemma OAI.SharpPlanar.IntegerRoots.mid181_contains line 1204
742. def OAI.SharpPlanar.IntegerRoots.root181 line 1205
743. lemma OAI.SharpPlanar.IntegerRoots.root181_contains line 1206
744. def OAI.SharpPlanar.IntegerRoots.root182 line 1209
745. lemma OAI.SharpPlanar.IntegerRoots.root182_contains line 1210
746. def OAI.SharpPlanar.IntegerRoots.mid183 line 1213
747. lemma OAI.SharpPlanar.IntegerRoots.mid183_contains line 1214
748. def OAI.SharpPlanar.IntegerRoots.root183 line 1215
749. lemma OAI.SharpPlanar.IntegerRoots.root183_contains line 1216
750. def OAI.SharpPlanar.IntegerRoots.root184 line 1219
751. lemma OAI.SharpPlanar.IntegerRoots.root184_contains line 1220
752. def OAI.SharpPlanar.IntegerRoots.mid185 line 1223
753. lemma OAI.SharpPlanar.IntegerRoots.mid185_contains line 1224
754. def OAI.SharpPlanar.IntegerRoots.root185 line 1225
755. lemma OAI.SharpPlanar.IntegerRoots.root185_contains line 1226
756. def OAI.SharpPlanar.IntegerRoots.root186 line 1229
757. lemma OAI.SharpPlanar.IntegerRoots.root186_contains line 1230
758. def OAI.SharpPlanar.IntegerRoots.mid187 line 1233
759. lemma OAI.SharpPlanar.IntegerRoots.mid187_contains line 1234
760. def OAI.SharpPlanar.IntegerRoots.root187 line 1235
761. lemma OAI.SharpPlanar.IntegerRoots.root187_contains line 1236
762. def OAI.SharpPlanar.IntegerRoots.root188 line 1239
763. lemma OAI.SharpPlanar.IntegerRoots.root188_contains line 1240
764. def OAI.SharpPlanar.IntegerRoots.mid189 line 1243
765. lemma OAI.SharpPlanar.IntegerRoots.mid189_contains line 1244
766. def OAI.SharpPlanar.IntegerRoots.root189 line 1245
767. lemma OAI.SharpPlanar.IntegerRoots.root189_contains line 1246
768. def OAI.SharpPlanar.IntegerRoots.root190 line 1249
769. lemma OAI.SharpPlanar.IntegerRoots.root190_contains line 1250
770. def OAI.SharpPlanar.IntegerRoots.mid191 line 1253
771. lemma OAI.SharpPlanar.IntegerRoots.mid191_contains line 1254
772. def OAI.SharpPlanar.IntegerRoots.root191 line 1255
773. lemma OAI.SharpPlanar.IntegerRoots.root191_contains line 1256
774. def OAI.SharpPlanar.IntegerRoots.root192 line 1259
775. lemma OAI.SharpPlanar.IntegerRoots.root192_contains line 1260
776. def OAI.SharpPlanar.IntegerRoots.mid193 line 1263
777. lemma OAI.SharpPlanar.IntegerRoots.mid193_contains line 1264
778. def OAI.SharpPlanar.IntegerRoots.root193 line 1265
779. lemma OAI.SharpPlanar.IntegerRoots.root193_contains line 1266
780. def OAI.SharpPlanar.IntegerRoots.root194 line 1269
781. lemma OAI.SharpPlanar.IntegerRoots.root194_contains line 1270
782. def OAI.SharpPlanar.IntegerRoots.mid195 line 1273
783. lemma OAI.SharpPlanar.IntegerRoots.mid195_contains line 1274
784. def OAI.SharpPlanar.IntegerRoots.root195 line 1275
785. lemma OAI.SharpPlanar.IntegerRoots.root195_contains line 1276
786. def OAI.SharpPlanar.IntegerRoots.root196 line 1279
787. lemma OAI.SharpPlanar.IntegerRoots.root196_contains line 1280
788. def OAI.SharpPlanar.IntegerRoots.mid197 line 1283
789. lemma OAI.SharpPlanar.IntegerRoots.mid197_contains line 1284
790. def OAI.SharpPlanar.IntegerRoots.root197 line 1285
791. lemma OAI.SharpPlanar.IntegerRoots.root197_contains line 1286
792. def OAI.SharpPlanar.IntegerRoots.root198 line 1289
793. lemma OAI.SharpPlanar.IntegerRoots.root198_contains line 1290
794. def OAI.SharpPlanar.IntegerRoots.mid199 line 1293
795. lemma OAI.SharpPlanar.IntegerRoots.mid199_contains line 1294
796. def OAI.SharpPlanar.IntegerRoots.root199 line 1295
797. lemma OAI.SharpPlanar.IntegerRoots.root199_contains line 1296
798. def OAI.SharpPlanar.IntegerRoots.root200 line 1299
799. lemma OAI.SharpPlanar.IntegerRoots.root200_contains line 1300
800. def OAI.SharpPlanar.IntegerRoots.mid201 line 1303
801. lemma OAI.SharpPlanar.IntegerRoots.mid201_contains line 1304
802. def OAI.SharpPlanar.IntegerRoots.root201 line 1305
803. lemma OAI.SharpPlanar.IntegerRoots.root201_contains line 1306
804. def OAI.SharpPlanar.IntegerRoots.root202 line 1309
805. lemma OAI.SharpPlanar.IntegerRoots.root202_contains line 1310
806. def OAI.SharpPlanar.IntegerRoots.mid203 line 1313
807. lemma OAI.SharpPlanar.IntegerRoots.mid203_contains line 1314
808. def OAI.SharpPlanar.IntegerRoots.root203 line 1315
809. lemma OAI.SharpPlanar.IntegerRoots.root203_contains line 1316
810. def OAI.SharpPlanar.IntegerRoots.root204 line 1319
811. lemma OAI.SharpPlanar.IntegerRoots.root204_contains line 1320
812. def OAI.SharpPlanar.IntegerRoots.mid205 line 1323
813. lemma OAI.SharpPlanar.IntegerRoots.mid205_contains line 1324
814. def OAI.SharpPlanar.IntegerRoots.root205 line 1325
815. lemma OAI.SharpPlanar.IntegerRoots.root205_contains line 1326
816. def OAI.SharpPlanar.IntegerRoots.root206 line 1329
817. lemma OAI.SharpPlanar.IntegerRoots.root206_contains line 1330
818. def OAI.SharpPlanar.IntegerRoots.mid207 line 1333
819. lemma OAI.SharpPlanar.IntegerRoots.mid207_contains line 1334
820. def OAI.SharpPlanar.IntegerRoots.root207 line 1335
821. lemma OAI.SharpPlanar.IntegerRoots.root207_contains line 1336
822. def OAI.SharpPlanar.IntegerRoots.root208 line 1339
823. lemma OAI.SharpPlanar.IntegerRoots.root208_contains line 1340
824. def OAI.SharpPlanar.IntegerRoots.mid209 line 1343
825. lemma OAI.SharpPlanar.IntegerRoots.mid209_contains line 1344
826. def OAI.SharpPlanar.IntegerRoots.root209 line 1345
827. lemma OAI.SharpPlanar.IntegerRoots.root209_contains line 1346
828. def OAI.SharpPlanar.IntegerRoots.root210 line 1349
829. lemma OAI.SharpPlanar.IntegerRoots.root210_contains line 1350
830. def OAI.SharpPlanar.IntegerRoots.mid211 line 1353
831. lemma OAI.SharpPlanar.IntegerRoots.mid211_contains line 1354
832. def OAI.SharpPlanar.IntegerRoots.root211 line 1355
833. lemma OAI.SharpPlanar.IntegerRoots.root211_contains line 1356
834. def OAI.SharpPlanar.IntegerRoots.root212 line 1359
835. lemma OAI.SharpPlanar.IntegerRoots.root212_contains line 1360
836. def OAI.SharpPlanar.IntegerRoots.mid213 line 1363
837. lemma OAI.SharpPlanar.IntegerRoots.mid213_contains line 1364
838. def OAI.SharpPlanar.IntegerRoots.root213 line 1365
839. lemma OAI.SharpPlanar.IntegerRoots.root213_contains line 1366
840. def OAI.SharpPlanar.IntegerRoots.root214 line 1369
841. lemma OAI.SharpPlanar.IntegerRoots.root214_contains line 1370
842. def OAI.SharpPlanar.IntegerRoots.mid215 line 1373
843. lemma OAI.SharpPlanar.IntegerRoots.mid215_contains line 1374
844. def OAI.SharpPlanar.IntegerRoots.root215 line 1375
845. lemma OAI.SharpPlanar.IntegerRoots.root215_contains line 1376
846. def OAI.SharpPlanar.IntegerRoots.root216 line 1379
847. lemma OAI.SharpPlanar.IntegerRoots.root216_contains line 1380
848. def OAI.SharpPlanar.IntegerRoots.mid217 line 1383
849. lemma OAI.SharpPlanar.IntegerRoots.mid217_contains line 1384
850. def OAI.SharpPlanar.IntegerRoots.root217 line 1385
851. lemma OAI.SharpPlanar.IntegerRoots.root217_contains line 1386
852. def OAI.SharpPlanar.IntegerRoots.root218 line 1389
853. lemma OAI.SharpPlanar.IntegerRoots.root218_contains line 1390
854. def OAI.SharpPlanar.IntegerRoots.mid219 line 1393
855. lemma OAI.SharpPlanar.IntegerRoots.mid219_contains line 1394
856. def OAI.SharpPlanar.IntegerRoots.root219 line 1395
857. lemma OAI.SharpPlanar.IntegerRoots.root219_contains line 1396
858. def OAI.SharpPlanar.IntegerRoots.root220 line 1399
859. lemma OAI.SharpPlanar.IntegerRoots.root220_contains line 1400
860. def OAI.SharpPlanar.IntegerRoots.mid221 line 1403
861. lemma OAI.SharpPlanar.IntegerRoots.mid221_contains line 1404
862. def OAI.SharpPlanar.IntegerRoots.root221 line 1405
863. lemma OAI.SharpPlanar.IntegerRoots.root221_contains line 1406
864. def OAI.SharpPlanar.IntegerRoots.root222 line 1409
865. lemma OAI.SharpPlanar.IntegerRoots.root222_contains line 1410
866. def OAI.SharpPlanar.IntegerRoots.mid223 line 1413
867. lemma OAI.SharpPlanar.IntegerRoots.mid223_contains line 1414
868. def OAI.SharpPlanar.IntegerRoots.root223 line 1415
869. lemma OAI.SharpPlanar.IntegerRoots.root223_contains line 1416
870. def OAI.SharpPlanar.IntegerRoots.root224 line 1419
871. lemma OAI.SharpPlanar.IntegerRoots.root224_contains line 1420
872. def OAI.SharpPlanar.IntegerRoots.mid225 line 1423
873. lemma OAI.SharpPlanar.IntegerRoots.mid225_contains line 1424
874. def OAI.SharpPlanar.IntegerRoots.root225 line 1425
875. lemma OAI.SharpPlanar.IntegerRoots.root225_contains line 1426
876. def OAI.SharpPlanar.IntegerRoots.root226 line 1429
877. lemma OAI.SharpPlanar.IntegerRoots.root226_contains line 1430
878. def OAI.SharpPlanar.IntegerRoots.mid227 line 1433
879. lemma OAI.SharpPlanar.IntegerRoots.mid227_contains line 1434
880. def OAI.SharpPlanar.IntegerRoots.root227 line 1435
881. lemma OAI.SharpPlanar.IntegerRoots.root227_contains line 1436
882. def OAI.SharpPlanar.IntegerRoots.root228 line 1439
883. lemma OAI.SharpPlanar.IntegerRoots.root228_contains line 1440
884. def OAI.SharpPlanar.IntegerRoots.mid229 line 1443
885. lemma OAI.SharpPlanar.IntegerRoots.mid229_contains line 1444
886. def OAI.SharpPlanar.IntegerRoots.root229 line 1445
887. lemma OAI.SharpPlanar.IntegerRoots.root229_contains line 1446
888. def OAI.SharpPlanar.IntegerRoots.root230 line 1449
889. lemma OAI.SharpPlanar.IntegerRoots.root230_contains line 1450
890. def OAI.SharpPlanar.IntegerRoots.mid231 line 1453
891. lemma OAI.SharpPlanar.IntegerRoots.mid231_contains line 1454
892. def OAI.SharpPlanar.IntegerRoots.root231 line 1455
893. lemma OAI.SharpPlanar.IntegerRoots.root231_contains line 1456
894. def OAI.SharpPlanar.IntegerRoots.root232 line 1459
895. lemma OAI.SharpPlanar.IntegerRoots.root232_contains line 1460
896. def OAI.SharpPlanar.IntegerRoots.mid233 line 1463
897. lemma OAI.SharpPlanar.IntegerRoots.mid233_contains line 1464
898. def OAI.SharpPlanar.IntegerRoots.root233 line 1465
899. lemma OAI.SharpPlanar.IntegerRoots.root233_contains line 1466
900. def OAI.SharpPlanar.IntegerRoots.root234 line 1469
901. lemma OAI.SharpPlanar.IntegerRoots.root234_contains line 1470
902. def OAI.SharpPlanar.IntegerRoots.mid235 line 1473
903. lemma OAI.SharpPlanar.IntegerRoots.mid235_contains line 1474
904. def OAI.SharpPlanar.IntegerRoots.root235 line 1475
905. lemma OAI.SharpPlanar.IntegerRoots.root235_contains line 1476
906. def OAI.SharpPlanar.IntegerRoots.root236 line 1479
907. lemma OAI.SharpPlanar.IntegerRoots.root236_contains line 1480
908. def OAI.SharpPlanar.IntegerRoots.mid237 line 1483
909. lemma OAI.SharpPlanar.IntegerRoots.mid237_contains line 1484
910. def OAI.SharpPlanar.IntegerRoots.root237 line 1485
911. lemma OAI.SharpPlanar.IntegerRoots.root237_contains line 1486
912. def OAI.SharpPlanar.IntegerRoots.root238 line 1489
913. lemma OAI.SharpPlanar.IntegerRoots.root238_contains line 1490
914. def OAI.SharpPlanar.IntegerRoots.mid239 line 1493
915. lemma OAI.SharpPlanar.IntegerRoots.mid239_contains line 1494
916. def OAI.SharpPlanar.IntegerRoots.root239 line 1495
917. lemma OAI.SharpPlanar.IntegerRoots.root239_contains line 1496
918. def OAI.SharpPlanar.IntegerRoots.root240 line 1499
919. lemma OAI.SharpPlanar.IntegerRoots.root240_contains line 1500
920. def OAI.SharpPlanar.IntegerRoots.mid241 line 1503
921. lemma OAI.SharpPlanar.IntegerRoots.mid241_contains line 1504
922. def OAI.SharpPlanar.IntegerRoots.root241 line 1505
923. lemma OAI.SharpPlanar.IntegerRoots.root241_contains line 1506
924. def OAI.SharpPlanar.IntegerRoots.root242 line 1509
925. lemma OAI.SharpPlanar.IntegerRoots.root242_contains line 1510
926. def OAI.SharpPlanar.IntegerRoots.mid243 line 1513
927. lemma OAI.SharpPlanar.IntegerRoots.mid243_contains line 1514
928. def OAI.SharpPlanar.IntegerRoots.root243 line 1515
929. lemma OAI.SharpPlanar.IntegerRoots.root243_contains line 1516
930. def OAI.SharpPlanar.IntegerRoots.root244 line 1519
931. lemma OAI.SharpPlanar.IntegerRoots.root244_contains line 1520
932. def OAI.SharpPlanar.IntegerRoots.mid245 line 1523
933. lemma OAI.SharpPlanar.IntegerRoots.mid245_contains line 1524
934. def OAI.SharpPlanar.IntegerRoots.root245 line 1525
935. lemma OAI.SharpPlanar.IntegerRoots.root245_contains line 1526
936. def OAI.SharpPlanar.IntegerRoots.root246 line 1529
937. lemma OAI.SharpPlanar.IntegerRoots.root246_contains line 1530
938. def OAI.SharpPlanar.IntegerRoots.mid247 line 1533
939. lemma OAI.SharpPlanar.IntegerRoots.mid247_contains line 1534
940. def OAI.SharpPlanar.IntegerRoots.root247 line 1535
941. lemma OAI.SharpPlanar.IntegerRoots.root247_contains line 1536
942. def OAI.SharpPlanar.IntegerRoots.root248 line 1539
943. lemma OAI.SharpPlanar.IntegerRoots.root248_contains line 1540
944. def OAI.SharpPlanar.IntegerRoots.mid249 line 1543
945. lemma OAI.SharpPlanar.IntegerRoots.mid249_contains line 1544
946. def OAI.SharpPlanar.IntegerRoots.root249 line 1545
947. lemma OAI.SharpPlanar.IntegerRoots.root249_contains line 1546
948. def OAI.SharpPlanar.IntegerRoots.root250 line 1549
949. lemma OAI.SharpPlanar.IntegerRoots.root250_contains line 1550
950. def OAI.SharpPlanar.IntegerRoots.mid251 line 1553
951. lemma OAI.SharpPlanar.IntegerRoots.mid251_contains line 1554
952. def OAI.SharpPlanar.IntegerRoots.root251 line 1555
953. lemma OAI.SharpPlanar.IntegerRoots.root251_contains line 1556
954. def OAI.SharpPlanar.IntegerRoots.root252 line 1559
955. lemma OAI.SharpPlanar.IntegerRoots.root252_contains line 1560
956. def OAI.SharpPlanar.IntegerRoots.mid253 line 1563
957. lemma OAI.SharpPlanar.IntegerRoots.mid253_contains line 1564
958. def OAI.SharpPlanar.IntegerRoots.root253 line 1565
959. lemma OAI.SharpPlanar.IntegerRoots.root253_contains line 1566
960. def OAI.SharpPlanar.IntegerRoots.root254 line 1569
961. lemma OAI.SharpPlanar.IntegerRoots.root254_contains line 1570
962. def OAI.SharpPlanar.IntegerRoots.mid255 line 1573
963. lemma OAI.SharpPlanar.IntegerRoots.mid255_contains line 1574
964. def OAI.SharpPlanar.IntegerRoots.root255 line 1575
965. lemma OAI.SharpPlanar.IntegerRoots.root255_contains line 1576
966. def OAI.SharpPlanar.IntegerRoots.root256 line 1579
967. lemma OAI.SharpPlanar.IntegerRoots.root256_contains line 1580
968. def OAI.SharpPlanar.IntegerRoots.mid257 line 1583
969. lemma OAI.SharpPlanar.IntegerRoots.mid257_contains line 1584
970. def OAI.SharpPlanar.IntegerRoots.root257 line 1585
971. lemma OAI.SharpPlanar.IntegerRoots.root257_contains line 1586
972. def OAI.SharpPlanar.IntegerRoots.root258 line 1589
973. lemma OAI.SharpPlanar.IntegerRoots.root258_contains line 1590
974. def OAI.SharpPlanar.IntegerRoots.mid259 line 1593
975. lemma OAI.SharpPlanar.IntegerRoots.mid259_contains line 1594
976. def OAI.SharpPlanar.IntegerRoots.root259 line 1595
977. lemma OAI.SharpPlanar.IntegerRoots.root259_contains line 1596
978. def OAI.SharpPlanar.IntegerRoots.root260 line 1599
979. lemma OAI.SharpPlanar.IntegerRoots.root260_contains line 1600
980. def OAI.SharpPlanar.IntegerRoots.mid261 line 1603
981. lemma OAI.SharpPlanar.IntegerRoots.mid261_contains line 1604
982. def OAI.SharpPlanar.IntegerRoots.root261 line 1605
983. lemma OAI.SharpPlanar.IntegerRoots.root261_contains line 1606
984. def OAI.SharpPlanar.IntegerRoots.root262 line 1609
985. lemma OAI.SharpPlanar.IntegerRoots.root262_contains line 1610
986. def OAI.SharpPlanar.IntegerRoots.mid263 line 1613
987. lemma OAI.SharpPlanar.IntegerRoots.mid263_contains line 1614
988. def OAI.SharpPlanar.IntegerRoots.root263 line 1615
989. lemma OAI.SharpPlanar.IntegerRoots.root263_contains line 1616
990. def OAI.SharpPlanar.IntegerRoots.root264 line 1619
991. lemma OAI.SharpPlanar.IntegerRoots.root264_contains line 1620
992. def OAI.SharpPlanar.IntegerRoots.mid265 line 1623
993. lemma OAI.SharpPlanar.IntegerRoots.mid265_contains line 1624
994. def OAI.SharpPlanar.IntegerRoots.root265 line 1625
995. lemma OAI.SharpPlanar.IntegerRoots.root265_contains line 1626
996. def OAI.SharpPlanar.IntegerRoots.root266 line 1629
997. lemma OAI.SharpPlanar.IntegerRoots.root266_contains line 1630
998. def OAI.SharpPlanar.IntegerRoots.mid267 line 1633
999. lemma OAI.SharpPlanar.IntegerRoots.mid267_contains line 1634
1000. def OAI.SharpPlanar.IntegerRoots.root267 line 1635
1001. lemma OAI.SharpPlanar.IntegerRoots.root267_contains line 1636
1002. def OAI.SharpPlanar.IntegerRoots.root268 line 1639
1003. lemma OAI.SharpPlanar.IntegerRoots.root268_contains line 1640
1004. def OAI.SharpPlanar.IntegerRoots.mid269 line 1643
1005. lemma OAI.SharpPlanar.IntegerRoots.mid269_contains line 1644
1006. def OAI.SharpPlanar.IntegerRoots.root269 line 1645
1007. lemma OAI.SharpPlanar.IntegerRoots.root269_contains line 1646
1008. def OAI.SharpPlanar.IntegerRoots.root270 line 1649
1009. lemma OAI.SharpPlanar.IntegerRoots.root270_contains line 1650
1010. def OAI.SharpPlanar.IntegerRoots.mid271 line 1653
1011. lemma OAI.SharpPlanar.IntegerRoots.mid271_contains line 1654
1012. def OAI.SharpPlanar.IntegerRoots.root271 line 1655
1013. lemma OAI.SharpPlanar.IntegerRoots.root271_contains line 1656
1014. def OAI.SharpPlanar.IntegerRoots.root272 line 1659
1015. lemma OAI.SharpPlanar.IntegerRoots.root272_contains line 1660
1016. def OAI.SharpPlanar.IntegerRoots.mid273 line 1663
1017. lemma OAI.SharpPlanar.IntegerRoots.mid273_contains line 1664
1018. def OAI.SharpPlanar.IntegerRoots.root273 line 1665
1019. lemma OAI.SharpPlanar.IntegerRoots.root273_contains line 1666
1020. def OAI.SharpPlanar.IntegerRoots.root274 line 1669
1021. lemma OAI.SharpPlanar.IntegerRoots.root274_contains line 1670
1022. def OAI.SharpPlanar.IntegerRoots.mid275 line 1673
1023. lemma OAI.SharpPlanar.IntegerRoots.mid275_contains line 1674
1024. def OAI.SharpPlanar.IntegerRoots.root275 line 1675
1025. lemma OAI.SharpPlanar.IntegerRoots.root275_contains line 1676
1026. def OAI.SharpPlanar.IntegerRoots.root276 line 1679
1027. lemma OAI.SharpPlanar.IntegerRoots.root276_contains line 1680
1028. def OAI.SharpPlanar.IntegerRoots.mid277 line 1683
1029. lemma OAI.SharpPlanar.IntegerRoots.mid277_contains line 1684
1030. def OAI.SharpPlanar.IntegerRoots.root277 line 1685
1031. lemma OAI.SharpPlanar.IntegerRoots.root277_contains line 1686
1032. def OAI.SharpPlanar.IntegerRoots.root278 line 1689
1033. lemma OAI.SharpPlanar.IntegerRoots.root278_contains line 1690
1034. def OAI.SharpPlanar.IntegerRoots.mid279 line 1693
1035. lemma OAI.SharpPlanar.IntegerRoots.mid279_contains line 1694
1036. def OAI.SharpPlanar.IntegerRoots.root279 line 1695
1037. lemma OAI.SharpPlanar.IntegerRoots.root279_contains line 1696
1038. def OAI.SharpPlanar.IntegerRoots.root280 line 1699
1039. lemma OAI.SharpPlanar.IntegerRoots.root280_contains line 1700
1040. def OAI.SharpPlanar.IntegerRoots.mid281 line 1703
1041. lemma OAI.SharpPlanar.IntegerRoots.mid281_contains line 1704
1042. def OAI.SharpPlanar.IntegerRoots.root281 line 1705
1043. lemma OAI.SharpPlanar.IntegerRoots.root281_contains line 1706
1044. def OAI.SharpPlanar.IntegerRoots.root282 line 1709
1045. lemma OAI.SharpPlanar.IntegerRoots.root282_contains line 1710
1046. def OAI.SharpPlanar.IntegerRoots.mid283 line 1713
1047. lemma OAI.SharpPlanar.IntegerRoots.mid283_contains line 1714
1048. def OAI.SharpPlanar.IntegerRoots.root283 line 1715
1049. lemma OAI.SharpPlanar.IntegerRoots.root283_contains line 1716
1050. def OAI.SharpPlanar.IntegerRoots.root284 line 1719
1051. lemma OAI.SharpPlanar.IntegerRoots.root284_contains line 1720
1052. def OAI.SharpPlanar.IntegerRoots.mid285 line 1723
1053. lemma OAI.SharpPlanar.IntegerRoots.mid285_contains line 1724
1054. def OAI.SharpPlanar.IntegerRoots.root285 line 1725
1055. lemma OAI.SharpPlanar.IntegerRoots.root285_contains line 1726
1056. def OAI.SharpPlanar.IntegerRoots.root286 line 1729
1057. lemma OAI.SharpPlanar.IntegerRoots.root286_contains line 1730
1058. def OAI.SharpPlanar.IntegerRoots.mid287 line 1733
1059. lemma OAI.SharpPlanar.IntegerRoots.mid287_contains line 1734
1060. def OAI.SharpPlanar.IntegerRoots.root287 line 1735
1061. lemma OAI.SharpPlanar.IntegerRoots.root287_contains line 1736
1062. def OAI.SharpPlanar.IntegerRoots.root288 line 1739
1063. lemma OAI.SharpPlanar.IntegerRoots.root288_contains line 1740
1064. def OAI.SharpPlanar.IntegerRoots.mid289 line 1743
1065. lemma OAI.SharpPlanar.IntegerRoots.mid289_contains line 1744
1066. def OAI.SharpPlanar.IntegerRoots.root289 line 1745
1067. lemma OAI.SharpPlanar.IntegerRoots.root289_contains line 1746
1068. def OAI.SharpPlanar.IntegerRoots.root290 line 1749
1069. lemma OAI.SharpPlanar.IntegerRoots.root290_contains line 1750
1070. def OAI.SharpPlanar.IntegerRoots.mid291 line 1753
1071. lemma OAI.SharpPlanar.IntegerRoots.mid291_contains line 1754
1072. def OAI.SharpPlanar.IntegerRoots.root291 line 1755
1073. lemma OAI.SharpPlanar.IntegerRoots.root291_contains line 1756
1074. def OAI.SharpPlanar.IntegerRoots.root292 line 1759
1075. lemma OAI.SharpPlanar.IntegerRoots.root292_contains line 1760
1076. def OAI.SharpPlanar.IntegerRoots.mid293 line 1763
1077. lemma OAI.SharpPlanar.IntegerRoots.mid293_contains line 1764
1078. def OAI.SharpPlanar.IntegerRoots.root293 line 1765
1079. lemma OAI.SharpPlanar.IntegerRoots.root293_contains line 1766
1080. def OAI.SharpPlanar.IntegerRoots.root294 line 1769
1081. lemma OAI.SharpPlanar.IntegerRoots.root294_contains line 1770
1082. def OAI.SharpPlanar.IntegerRoots.mid295 line 1773
1083. lemma OAI.SharpPlanar.IntegerRoots.mid295_contains line 1774
1084. def OAI.SharpPlanar.IntegerRoots.root295 line 1775
1085. lemma OAI.SharpPlanar.IntegerRoots.root295_contains line 1776
1086. def OAI.SharpPlanar.IntegerRoots.root296 line 1779
1087. lemma OAI.SharpPlanar.IntegerRoots.root296_contains line 1780
1088. def OAI.SharpPlanar.IntegerRoots.mid297 line 1783
1089. lemma OAI.SharpPlanar.IntegerRoots.mid297_contains line 1784
1090. def OAI.SharpPlanar.IntegerRoots.root297 line 1785
1091. lemma OAI.SharpPlanar.IntegerRoots.root297_contains line 1786
1092. def OAI.SharpPlanar.IntegerRoots.root298 line 1789
1093. lemma OAI.SharpPlanar.IntegerRoots.root298_contains line 1790
1094. def OAI.SharpPlanar.IntegerRoots.mid299 line 1793
1095. lemma OAI.SharpPlanar.IntegerRoots.mid299_contains line 1794
1096. def OAI.SharpPlanar.IntegerRoots.root299 line 1795
1097. lemma OAI.SharpPlanar.IntegerRoots.root299_contains line 1796
1098. def OAI.SharpPlanar.IntegerRoots.root300 line 1799
1099. lemma OAI.SharpPlanar.IntegerRoots.root300_contains line 1800
1100. def OAI.SharpPlanar.IntegerRoots.mid301 line 1803
1101. lemma OAI.SharpPlanar.IntegerRoots.mid301_contains line 1804
1102. def OAI.SharpPlanar.IntegerRoots.root301 line 1805
1103. lemma OAI.SharpPlanar.IntegerRoots.root301_contains line 1806
1104. def OAI.SharpPlanar.IntegerRoots.root302 line 1809
1105. lemma OAI.SharpPlanar.IntegerRoots.root302_contains line 1810
1106. def OAI.SharpPlanar.IntegerRoots.mid303 line 1813
1107. lemma OAI.SharpPlanar.IntegerRoots.mid303_contains line 1814
1108. def OAI.SharpPlanar.IntegerRoots.root303 line 1815
1109. lemma OAI.SharpPlanar.IntegerRoots.root303_contains line 1816
1110. def OAI.SharpPlanar.IntegerRoots.root304 line 1819
1111. lemma OAI.SharpPlanar.IntegerRoots.root304_contains line 1820
1112. def OAI.SharpPlanar.IntegerRoots.mid305 line 1823
1113. lemma OAI.SharpPlanar.IntegerRoots.mid305_contains line 1824
1114. def OAI.SharpPlanar.IntegerRoots.root305 line 1825
1115. lemma OAI.SharpPlanar.IntegerRoots.root305_contains line 1826
1116. def OAI.SharpPlanar.IntegerRoots.root306 line 1829
1117. lemma OAI.SharpPlanar.IntegerRoots.root306_contains line 1830
1118. def OAI.SharpPlanar.IntegerRoots.mid307 line 1833
1119. lemma OAI.SharpPlanar.IntegerRoots.mid307_contains line 1834
1120. def OAI.SharpPlanar.IntegerRoots.root307 line 1835
1121. lemma OAI.SharpPlanar.IntegerRoots.root307_contains line 1836
1122. def OAI.SharpPlanar.IntegerRoots.root308 line 1839
1123. lemma OAI.SharpPlanar.IntegerRoots.root308_contains line 1840
1124. def OAI.SharpPlanar.IntegerRoots.mid309 line 1843
1125. lemma OAI.SharpPlanar.IntegerRoots.mid309_contains line 1844
1126. def OAI.SharpPlanar.IntegerRoots.root309 line 1845
1127. lemma OAI.SharpPlanar.IntegerRoots.root309_contains line 1846
1128. def OAI.SharpPlanar.IntegerRoots.root310 line 1849
1129. lemma OAI.SharpPlanar.IntegerRoots.root310_contains line 1850
1130. def OAI.SharpPlanar.IntegerRoots.mid311 line 1853
1131. lemma OAI.SharpPlanar.IntegerRoots.mid311_contains line 1854
1132. def OAI.SharpPlanar.IntegerRoots.root311 line 1855
1133. lemma OAI.SharpPlanar.IntegerRoots.root311_contains line 1856
1134. def OAI.SharpPlanar.IntegerRoots.root312 line 1859
1135. lemma OAI.SharpPlanar.IntegerRoots.root312_contains line 1860
1136. def OAI.SharpPlanar.IntegerRoots.mid313 line 1863
1137. lemma OAI.SharpPlanar.IntegerRoots.mid313_contains line 1864
1138. def OAI.SharpPlanar.IntegerRoots.root313 line 1865
1139. lemma OAI.SharpPlanar.IntegerRoots.root313_contains line 1866
1140. def OAI.SharpPlanar.IntegerRoots.root314 line 1869
1141. lemma OAI.SharpPlanar.IntegerRoots.root314_contains line 1870
1142. def OAI.SharpPlanar.IntegerRoots.mid315 line 1873
1143. lemma OAI.SharpPlanar.IntegerRoots.mid315_contains line 1874
1144. def OAI.SharpPlanar.IntegerRoots.root315 line 1875
1145. lemma OAI.SharpPlanar.IntegerRoots.root315_contains line 1876
1146. def OAI.SharpPlanar.IntegerRoots.root316 line 1879
1147. lemma OAI.SharpPlanar.IntegerRoots.root316_contains line 1880
1148. def OAI.SharpPlanar.IntegerRoots.mid317 line 1883
1149. lemma OAI.SharpPlanar.IntegerRoots.mid317_contains line 1884
1150. def OAI.SharpPlanar.IntegerRoots.root317 line 1885
1151. lemma OAI.SharpPlanar.IntegerRoots.root317_contains line 1886
1152. def OAI.SharpPlanar.IntegerRoots.root318 line 1889
1153. lemma OAI.SharpPlanar.IntegerRoots.root318_contains line 1890
1154. def OAI.SharpPlanar.IntegerRoots.mid319 line 1893
1155. lemma OAI.SharpPlanar.IntegerRoots.mid319_contains line 1894
1156. def OAI.SharpPlanar.IntegerRoots.root319 line 1895
1157. lemma OAI.SharpPlanar.IntegerRoots.root319_contains line 1896
1158. def OAI.SharpPlanar.IntegerRoots.root320 line 1899
1159. lemma OAI.SharpPlanar.IntegerRoots.root320_contains line 1900
1160. def OAI.SharpPlanar.IntegerRoots.mid321 line 1903
1161. lemma OAI.SharpPlanar.IntegerRoots.mid321_contains line 1904
1162. def OAI.SharpPlanar.IntegerRoots.root321 line 1905
1163. lemma OAI.SharpPlanar.IntegerRoots.root321_contains line 1906
1164. def OAI.SharpPlanar.IntegerRoots.root322 line 1909
1165. lemma OAI.SharpPlanar.IntegerRoots.root322_contains line 1910
1166. def OAI.SharpPlanar.IntegerRoots.mid323 line 1913
1167. lemma OAI.SharpPlanar.IntegerRoots.mid323_contains line 1914
1168. def OAI.SharpPlanar.IntegerRoots.root323 line 1915
1169. lemma OAI.SharpPlanar.IntegerRoots.root323_contains line 1916
1170. def OAI.SharpPlanar.IntegerRoots.root324 line 1919
1171. lemma OAI.SharpPlanar.IntegerRoots.root324_contains line 1920
1172. def OAI.SharpPlanar.IntegerRoots.mid325 line 1923
1173. lemma OAI.SharpPlanar.IntegerRoots.mid325_contains line 1924
1174. def OAI.SharpPlanar.IntegerRoots.root325 line 1925
1175. lemma OAI.SharpPlanar.IntegerRoots.root325_contains line 1926
1176. def OAI.SharpPlanar.IntegerRoots.root326 line 1929
1177. lemma OAI.SharpPlanar.IntegerRoots.root326_contains line 1930
1178. def OAI.SharpPlanar.IntegerRoots.mid327 line 1933
1179. lemma OAI.SharpPlanar.IntegerRoots.mid327_contains line 1934
1180. def OAI.SharpPlanar.IntegerRoots.root327 line 1935
1181. lemma OAI.SharpPlanar.IntegerRoots.root327_contains line 1936
1182. def OAI.SharpPlanar.IntegerRoots.root328 line 1939
1183. lemma OAI.SharpPlanar.IntegerRoots.root328_contains line 1940
1184. def OAI.SharpPlanar.IntegerRoots.mid329 line 1943
1185. lemma OAI.SharpPlanar.IntegerRoots.mid329_contains line 1944
1186. def OAI.SharpPlanar.IntegerRoots.root329 line 1945
1187. lemma OAI.SharpPlanar.IntegerRoots.root329_contains line 1946
1188. def OAI.SharpPlanar.IntegerRoots.root330 line 1949
1189. lemma OAI.SharpPlanar.IntegerRoots.root330_contains line 1950
1190. def OAI.SharpPlanar.IntegerRoots.mid331 line 1953
1191. lemma OAI.SharpPlanar.IntegerRoots.mid331_contains line 1954
1192. def OAI.SharpPlanar.IntegerRoots.root331 line 1955
1193. lemma OAI.SharpPlanar.IntegerRoots.root331_contains line 1956
1194. def OAI.SharpPlanar.IntegerRoots.root332 line 1959
1195. lemma OAI.SharpPlanar.IntegerRoots.root332_contains line 1960
1196. def OAI.SharpPlanar.IntegerRoots.mid333 line 1963
1197. lemma OAI.SharpPlanar.IntegerRoots.mid333_contains line 1964
1198. def OAI.SharpPlanar.IntegerRoots.root333 line 1965
1199. lemma OAI.SharpPlanar.IntegerRoots.root333_contains line 1966
1200. def OAI.SharpPlanar.IntegerRoots.root334 line 1969
1201. lemma OAI.SharpPlanar.IntegerRoots.root334_contains line 1970
1202. def OAI.SharpPlanar.IntegerRoots.mid335 line 1973
1203. lemma OAI.SharpPlanar.IntegerRoots.mid335_contains line 1974
1204. def OAI.SharpPlanar.IntegerRoots.root335 line 1975
1205. lemma OAI.SharpPlanar.IntegerRoots.root335_contains line 1976
1206. def OAI.SharpPlanar.IntegerRoots.root336 line 1979
1207. lemma OAI.SharpPlanar.IntegerRoots.root336_contains line 1980
1208. def OAI.SharpPlanar.IntegerRoots.mid337 line 1983
1209. lemma OAI.SharpPlanar.IntegerRoots.mid337_contains line 1984
1210. def OAI.SharpPlanar.IntegerRoots.root337 line 1985
1211. lemma OAI.SharpPlanar.IntegerRoots.root337_contains line 1986
1212. def OAI.SharpPlanar.IntegerRoots.root338 line 1989
1213. lemma OAI.SharpPlanar.IntegerRoots.root338_contains line 1990
1214. def OAI.SharpPlanar.IntegerRoots.mid339 line 1993
1215. lemma OAI.SharpPlanar.IntegerRoots.mid339_contains line 1994
1216. def OAI.SharpPlanar.IntegerRoots.root339 line 1995
1217. lemma OAI.SharpPlanar.IntegerRoots.root339_contains line 1996
1218. def OAI.SharpPlanar.IntegerRoots.root340 line 1999
1219. lemma OAI.SharpPlanar.IntegerRoots.root340_contains line 2000
1220. def OAI.SharpPlanar.IntegerRoots.mid341 line 2003
1221. lemma OAI.SharpPlanar.IntegerRoots.mid341_contains line 2004
1222. def OAI.SharpPlanar.IntegerRoots.root341 line 2005
1223. lemma OAI.SharpPlanar.IntegerRoots.root341_contains line 2006
1224. def OAI.SharpPlanar.IntegerRoots.root342 line 2009
1225. lemma OAI.SharpPlanar.IntegerRoots.root342_contains line 2010
1226. def OAI.SharpPlanar.IntegerRoots.mid343 line 2013
1227. lemma OAI.SharpPlanar.IntegerRoots.mid343_contains line 2014
1228. def OAI.SharpPlanar.IntegerRoots.root343 line 2015
1229. lemma OAI.SharpPlanar.IntegerRoots.root343_contains line 2016
1230. def OAI.SharpPlanar.IntegerRoots.root344 line 2019
1231. lemma OAI.SharpPlanar.IntegerRoots.root344_contains line 2020
1232. def OAI.SharpPlanar.IntegerRoots.mid345 line 2023
1233. lemma OAI.SharpPlanar.IntegerRoots.mid345_contains line 2024
1234. def OAI.SharpPlanar.IntegerRoots.root345 line 2025
1235. lemma OAI.SharpPlanar.IntegerRoots.root345_contains line 2026
1236. def OAI.SharpPlanar.IntegerRoots.root346 line 2029
1237. lemma OAI.SharpPlanar.IntegerRoots.root346_contains line 2030
1238. def OAI.SharpPlanar.IntegerRoots.mid347 line 2033
1239. lemma OAI.SharpPlanar.IntegerRoots.mid347_contains line 2034
1240. def OAI.SharpPlanar.IntegerRoots.root347 line 2035
1241. lemma OAI.SharpPlanar.IntegerRoots.root347_contains line 2036
1242. def OAI.SharpPlanar.IntegerRoots.root348 line 2039
1243. lemma OAI.SharpPlanar.IntegerRoots.root348_contains line 2040
1244. def OAI.SharpPlanar.IntegerRoots.mid349 line 2043
1245. lemma OAI.SharpPlanar.IntegerRoots.mid349_contains line 2044
1246. def OAI.SharpPlanar.IntegerRoots.root349 line 2045
1247. lemma OAI.SharpPlanar.IntegerRoots.root349_contains line 2046
1248. def OAI.SharpPlanar.IntegerRoots.root350 line 2049
1249. lemma OAI.SharpPlanar.IntegerRoots.root350_contains line 2050
1250. def OAI.SharpPlanar.IntegerRoots.mid351 line 2053
1251. lemma OAI.SharpPlanar.IntegerRoots.mid351_contains line 2054
1252. def OAI.SharpPlanar.IntegerRoots.root351 line 2055
1253. lemma OAI.SharpPlanar.IntegerRoots.root351_contains line 2056
1254. def OAI.SharpPlanar.IntegerRoots.root352 line 2059
1255. lemma OAI.SharpPlanar.IntegerRoots.root352_contains line 2060
1256. def OAI.SharpPlanar.IntegerRoots.mid353 line 2063
1257. lemma OAI.SharpPlanar.IntegerRoots.mid353_contains line 2064
1258. def OAI.SharpPlanar.IntegerRoots.root353 line 2065
1259. lemma OAI.SharpPlanar.IntegerRoots.root353_contains line 2066
1260. def OAI.SharpPlanar.IntegerRoots.root354 line 2069
1261. lemma OAI.SharpPlanar.IntegerRoots.root354_contains line 2070
1262. def OAI.SharpPlanar.IntegerRoots.mid355 line 2073
1263. lemma OAI.SharpPlanar.IntegerRoots.mid355_contains line 2074
1264. def OAI.SharpPlanar.IntegerRoots.root355 line 2075
1265. lemma OAI.SharpPlanar.IntegerRoots.root355_contains line 2076
1266. def OAI.SharpPlanar.IntegerRoots.root356 line 2079
1267. lemma OAI.SharpPlanar.IntegerRoots.root356_contains line 2080
1268. def OAI.SharpPlanar.IntegerRoots.mid357 line 2083
1269. lemma OAI.SharpPlanar.IntegerRoots.mid357_contains line 2084
1270. def OAI.SharpPlanar.IntegerRoots.root357 line 2085
1271. lemma OAI.SharpPlanar.IntegerRoots.root357_contains line 2086
1272. def OAI.SharpPlanar.IntegerRoots.root358 line 2089
1273. lemma OAI.SharpPlanar.IntegerRoots.root358_contains line 2090
1274. def OAI.SharpPlanar.IntegerRoots.mid359 line 2093
1275. lemma OAI.SharpPlanar.IntegerRoots.mid359_contains line 2094
1276. def OAI.SharpPlanar.IntegerRoots.root359 line 2095
1277. lemma OAI.SharpPlanar.IntegerRoots.root359_contains line 2096
1278. def OAI.SharpPlanar.IntegerRoots.root360 line 2099
1279. lemma OAI.SharpPlanar.IntegerRoots.root360_contains line 2100
1280. def OAI.SharpPlanar.IntegerRoots.mid361 line 2103
1281. lemma OAI.SharpPlanar.IntegerRoots.mid361_contains line 2104
1282. def OAI.SharpPlanar.IntegerRoots.root361 line 2105
1283. lemma OAI.SharpPlanar.IntegerRoots.root361_contains line 2106
1284. def OAI.SharpPlanar.IntegerRoots.root362 line 2109
1285. lemma OAI.SharpPlanar.IntegerRoots.root362_contains line 2110
1286. def OAI.SharpPlanar.IntegerRoots.mid363 line 2113
1287. lemma OAI.SharpPlanar.IntegerRoots.mid363_contains line 2114
1288. def OAI.SharpPlanar.IntegerRoots.root363 line 2115
1289. lemma OAI.SharpPlanar.IntegerRoots.root363_contains line 2116
1290. def OAI.SharpPlanar.IntegerRoots.root364 line 2119
1291. lemma OAI.SharpPlanar.IntegerRoots.root364_contains line 2120
1292. def OAI.SharpPlanar.IntegerRoots.mid365 line 2123
1293. lemma OAI.SharpPlanar.IntegerRoots.mid365_contains line 2124
1294. def OAI.SharpPlanar.IntegerRoots.root365 line 2125
1295. lemma OAI.SharpPlanar.IntegerRoots.root365_contains line 2126
1296. def OAI.SharpPlanar.IntegerRoots.root366 line 2129
1297. lemma OAI.SharpPlanar.IntegerRoots.root366_contains line 2130
1298. def OAI.SharpPlanar.IntegerRoots.mid367 line 2133
1299. lemma OAI.SharpPlanar.IntegerRoots.mid367_contains line 2134
1300. def OAI.SharpPlanar.IntegerRoots.root367 line 2135
1301. lemma OAI.SharpPlanar.IntegerRoots.root367_contains line 2136
1302. def OAI.SharpPlanar.IntegerRoots.root368 line 2139
1303. lemma OAI.SharpPlanar.IntegerRoots.root368_contains line 2140
1304. def OAI.SharpPlanar.IntegerRoots.mid369 line 2143
1305. lemma OAI.SharpPlanar.IntegerRoots.mid369_contains line 2144
1306. def OAI.SharpPlanar.IntegerRoots.root369 line 2145
1307. lemma OAI.SharpPlanar.IntegerRoots.root369_contains line 2146
1308. def OAI.SharpPlanar.IntegerRoots.root370 line 2149
1309. lemma OAI.SharpPlanar.IntegerRoots.root370_contains line 2150
1310. def OAI.SharpPlanar.IntegerRoots.mid371 line 2153
1311. lemma OAI.SharpPlanar.IntegerRoots.mid371_contains line 2154
1312. def OAI.SharpPlanar.IntegerRoots.root371 line 2155
1313. lemma OAI.SharpPlanar.IntegerRoots.root371_contains line 2156
1314. def OAI.SharpPlanar.IntegerRoots.root372 line 2159
1315. lemma OAI.SharpPlanar.IntegerRoots.root372_contains line 2160
1316. def OAI.SharpPlanar.IntegerRoots.mid373 line 2163
1317. lemma OAI.SharpPlanar.IntegerRoots.mid373_contains line 2164
1318. def OAI.SharpPlanar.IntegerRoots.root373 line 2165
1319. lemma OAI.SharpPlanar.IntegerRoots.root373_contains line 2166
1320. def OAI.SharpPlanar.IntegerRoots.root374 line 2169
1321. lemma OAI.SharpPlanar.IntegerRoots.root374_contains line 2170
1322. def OAI.SharpPlanar.IntegerRoots.mid375 line 2173
1323. lemma OAI.SharpPlanar.IntegerRoots.mid375_contains line 2174
1324. def OAI.SharpPlanar.IntegerRoots.root375 line 2175
1325. lemma OAI.SharpPlanar.IntegerRoots.root375_contains line 2176
1326. def OAI.SharpPlanar.IntegerRoots.root376 line 2179
1327. lemma OAI.SharpPlanar.IntegerRoots.root376_contains line 2180
1328. def OAI.SharpPlanar.IntegerRoots.mid377 line 2183
1329. lemma OAI.SharpPlanar.IntegerRoots.mid377_contains line 2184
1330. def OAI.SharpPlanar.IntegerRoots.root377 line 2185
1331. lemma OAI.SharpPlanar.IntegerRoots.root377_contains line 2186
1332. def OAI.SharpPlanar.IntegerRoots.root378 line 2189
1333. lemma OAI.SharpPlanar.IntegerRoots.root378_contains line 2190
1334. def OAI.SharpPlanar.IntegerRoots.mid379 line 2193
1335. lemma OAI.SharpPlanar.IntegerRoots.mid379_contains line 2194
1336. def OAI.SharpPlanar.IntegerRoots.root379 line 2195
1337. lemma OAI.SharpPlanar.IntegerRoots.root379_contains line 2196
1338. def OAI.SharpPlanar.IntegerRoots.root380 line 2199
1339. lemma OAI.SharpPlanar.IntegerRoots.root380_contains line 2200
1340. def OAI.SharpPlanar.IntegerRoots.mid381 line 2203
1341. lemma OAI.SharpPlanar.IntegerRoots.mid381_contains line 2204
1342. def OAI.SharpPlanar.IntegerRoots.root381 line 2205
1343. lemma OAI.SharpPlanar.IntegerRoots.root381_contains line 2206
1344. def OAI.SharpPlanar.IntegerRoots.root382 line 2209
1345. lemma OAI.SharpPlanar.IntegerRoots.root382_contains line 2210
1346. def OAI.SharpPlanar.IntegerRoots.mid383 line 2213
1347. lemma OAI.SharpPlanar.IntegerRoots.mid383_contains line 2214
1348. def OAI.SharpPlanar.IntegerRoots.root383 line 2215
1349. lemma OAI.SharpPlanar.IntegerRoots.root383_contains line 2216
1350. def OAI.SharpPlanar.IntegerRoots.root384 line 2219
1351. lemma OAI.SharpPlanar.IntegerRoots.root384_contains line 2220
1352. def OAI.SharpPlanar.IntegerRoots.mid385 line 2223
1353. lemma OAI.SharpPlanar.IntegerRoots.mid385_contains line 2224
1354. def OAI.SharpPlanar.IntegerRoots.root385 line 2225
1355. lemma OAI.SharpPlanar.IntegerRoots.root385_contains line 2226
1356. def OAI.SharpPlanar.IntegerRoots.root386 line 2229
1357. lemma OAI.SharpPlanar.IntegerRoots.root386_contains line 2230
1358. def OAI.SharpPlanar.IntegerRoots.mid387 line 2233
1359. lemma OAI.SharpPlanar.IntegerRoots.mid387_contains line 2234
1360. def OAI.SharpPlanar.IntegerRoots.root387 line 2235
1361. lemma OAI.SharpPlanar.IntegerRoots.root387_contains line 2236
1362. def OAI.SharpPlanar.IntegerRoots.root388 line 2239
1363. lemma OAI.SharpPlanar.IntegerRoots.root388_contains line 2240
1364. def OAI.SharpPlanar.IntegerRoots.mid389 line 2243
1365. lemma OAI.SharpPlanar.IntegerRoots.mid389_contains line 2244
1366. def OAI.SharpPlanar.IntegerRoots.root389 line 2245
1367. lemma OAI.SharpPlanar.IntegerRoots.root389_contains line 2246
1368. def OAI.SharpPlanar.IntegerRoots.root390 line 2249
1369. lemma OAI.SharpPlanar.IntegerRoots.root390_contains line 2250
1370. def OAI.SharpPlanar.IntegerRoots.mid391 line 2253
1371. lemma OAI.SharpPlanar.IntegerRoots.mid391_contains line 2254
1372. def OAI.SharpPlanar.IntegerRoots.root391 line 2255
1373. lemma OAI.SharpPlanar.IntegerRoots.root391_contains line 2256
1374. def OAI.SharpPlanar.IntegerRoots.root392 line 2259
1375. lemma OAI.SharpPlanar.IntegerRoots.root392_contains line 2260
1376. def OAI.SharpPlanar.IntegerRoots.mid393 line 2263
1377. lemma OAI.SharpPlanar.IntegerRoots.mid393_contains line 2264
1378. def OAI.SharpPlanar.IntegerRoots.root393 line 2265
1379. lemma OAI.SharpPlanar.IntegerRoots.root393_contains line 2266
1380. def OAI.SharpPlanar.IntegerRoots.root394 line 2269
1381. lemma OAI.SharpPlanar.IntegerRoots.root394_contains line 2270
1382. def OAI.SharpPlanar.IntegerRoots.mid395 line 2273
1383. lemma OAI.SharpPlanar.IntegerRoots.mid395_contains line 2274
1384. def OAI.SharpPlanar.IntegerRoots.root395 line 2275
1385. lemma OAI.SharpPlanar.IntegerRoots.root395_contains line 2276
1386. def OAI.SharpPlanar.IntegerRoots.root396 line 2279
1387. lemma OAI.SharpPlanar.IntegerRoots.root396_contains line 2280
1388. def OAI.SharpPlanar.IntegerRoots.mid397 line 2283
1389. lemma OAI.SharpPlanar.IntegerRoots.mid397_contains line 2284
1390. def OAI.SharpPlanar.IntegerRoots.root397 line 2285
1391. lemma OAI.SharpPlanar.IntegerRoots.root397_contains line 2286
1392. def OAI.SharpPlanar.IntegerRoots.root398 line 2289
1393. lemma OAI.SharpPlanar.IntegerRoots.root398_contains line 2290
1394. def OAI.SharpPlanar.IntegerRoots.mid399 line 2293
1395. lemma OAI.SharpPlanar.IntegerRoots.mid399_contains line 2294
1396. def OAI.SharpPlanar.IntegerRoots.root399 line 2295
1397. lemma OAI.SharpPlanar.IntegerRoots.root399_contains line 2296
1398. def OAI.SharpPlanar.IntegerRoots.root400 line 2299
1399. lemma OAI.SharpPlanar.IntegerRoots.root400_contains line 2300
1400. def OAI.SharpPlanar.IntegerRoots.mid401 line 2303
1401. lemma OAI.SharpPlanar.IntegerRoots.mid401_contains line 2304
1402. def OAI.SharpPlanar.IntegerRoots.root401 line 2305
1403. lemma OAI.SharpPlanar.IntegerRoots.root401_contains line 2306
1404. def OAI.SharpPlanar.IntegerRoots.root402 line 2309
1405. lemma OAI.SharpPlanar.IntegerRoots.root402_contains line 2310
1406. def OAI.SharpPlanar.IntegerRoots.mid403 line 2313
1407. lemma OAI.SharpPlanar.IntegerRoots.mid403_contains line 2314
1408. def OAI.SharpPlanar.IntegerRoots.root403 line 2315
1409. lemma OAI.SharpPlanar.IntegerRoots.root403_contains line 2316
1410. def OAI.SharpPlanar.IntegerRoots.root404 line 2319
1411. lemma OAI.SharpPlanar.IntegerRoots.root404_contains line 2320
1412. def OAI.SharpPlanar.IntegerRoots.mid405 line 2323
1413. lemma OAI.SharpPlanar.IntegerRoots.mid405_contains line 2324
1414. def OAI.SharpPlanar.IntegerRoots.root405 line 2325
1415. lemma OAI.SharpPlanar.IntegerRoots.root405_contains line 2326
1416. def OAI.SharpPlanar.IntegerRoots.root406 line 2329
1417. lemma OAI.SharpPlanar.IntegerRoots.root406_contains line 2330
1418. def OAI.SharpPlanar.IntegerRoots.mid407 line 2333
1419. lemma OAI.SharpPlanar.IntegerRoots.mid407_contains line 2334
1420. def OAI.SharpPlanar.IntegerRoots.root407 line 2335
1421. lemma OAI.SharpPlanar.IntegerRoots.root407_contains line 2336
1422. def OAI.SharpPlanar.IntegerRoots.root408 line 2339
1423. lemma OAI.SharpPlanar.IntegerRoots.root408_contains line 2340
1424. def OAI.SharpPlanar.IntegerRoots.mid409 line 2343
1425. lemma OAI.SharpPlanar.IntegerRoots.mid409_contains line 2344
1426. def OAI.SharpPlanar.IntegerRoots.root409 line 2345
1427. lemma OAI.SharpPlanar.IntegerRoots.root409_contains line 2346
1428. def OAI.SharpPlanar.IntegerRoots.root410 line 2349
1429. lemma OAI.SharpPlanar.IntegerRoots.root410_contains line 2350
1430. def OAI.SharpPlanar.IntegerRoots.mid411 line 2353
1431. lemma OAI.SharpPlanar.IntegerRoots.mid411_contains line 2354
1432. def OAI.SharpPlanar.IntegerRoots.root411 line 2355
1433. lemma OAI.SharpPlanar.IntegerRoots.root411_contains line 2356
1434. def OAI.SharpPlanar.IntegerRoots.root412 line 2359
1435. lemma OAI.SharpPlanar.IntegerRoots.root412_contains line 2360
1436. def OAI.SharpPlanar.IntegerRoots.mid413 line 2363
1437. lemma OAI.SharpPlanar.IntegerRoots.mid413_contains line 2364
1438. def OAI.SharpPlanar.IntegerRoots.root413 line 2365
1439. lemma OAI.SharpPlanar.IntegerRoots.root413_contains line 2366
1440. def OAI.SharpPlanar.IntegerRoots.root414 line 2369
1441. lemma OAI.SharpPlanar.IntegerRoots.root414_contains line 2370
1442. def OAI.SharpPlanar.IntegerRoots.mid415 line 2373
1443. lemma OAI.SharpPlanar.IntegerRoots.mid415_contains line 2374
1444. def OAI.SharpPlanar.IntegerRoots.root415 line 2375
1445. lemma OAI.SharpPlanar.IntegerRoots.root415_contains line 2376
1446. def OAI.SharpPlanar.IntegerRoots.root416 line 2379
1447. lemma OAI.SharpPlanar.IntegerRoots.root416_contains line 2380
1448. def OAI.SharpPlanar.IntegerRoots.mid417 line 2383
1449. lemma OAI.SharpPlanar.IntegerRoots.mid417_contains line 2384
1450. def OAI.SharpPlanar.IntegerRoots.root417 line 2385
1451. lemma OAI.SharpPlanar.IntegerRoots.root417_contains line 2386
1452. def OAI.SharpPlanar.IntegerRoots.root418 line 2389
1453. lemma OAI.SharpPlanar.IntegerRoots.root418_contains line 2390
1454. def OAI.SharpPlanar.IntegerRoots.mid419 line 2393
1455. lemma OAI.SharpPlanar.IntegerRoots.mid419_contains line 2394
1456. def OAI.SharpPlanar.IntegerRoots.root419 line 2395
1457. lemma OAI.SharpPlanar.IntegerRoots.root419_contains line 2396
1458. def OAI.SharpPlanar.IntegerRoots.root420 line 2399
1459. lemma OAI.SharpPlanar.IntegerRoots.root420_contains line 2400
1460. def OAI.SharpPlanar.IntegerRoots.mid421 line 2403
1461. lemma OAI.SharpPlanar.IntegerRoots.mid421_contains line 2404
1462. def OAI.SharpPlanar.IntegerRoots.root421 line 2405
1463. lemma OAI.SharpPlanar.IntegerRoots.root421_contains line 2406
1464. def OAI.SharpPlanar.IntegerRoots.root422 line 2409
1465. lemma OAI.SharpPlanar.IntegerRoots.root422_contains line 2410
1466. def OAI.SharpPlanar.IntegerRoots.mid423 line 2413
1467. lemma OAI.SharpPlanar.IntegerRoots.mid423_contains line 2414
1468. def OAI.SharpPlanar.IntegerRoots.root423 line 2415
1469. lemma OAI.SharpPlanar.IntegerRoots.root423_contains line 2416
1470. def OAI.SharpPlanar.IntegerRoots.root424 line 2419
1471. lemma OAI.SharpPlanar.IntegerRoots.root424_contains line 2420
1472. def OAI.SharpPlanar.IntegerRoots.mid425 line 2423
1473. lemma OAI.SharpPlanar.IntegerRoots.mid425_contains line 2424
1474. def OAI.SharpPlanar.IntegerRoots.root425 line 2425
1475. lemma OAI.SharpPlanar.IntegerRoots.root425_contains line 2426
1476. def OAI.SharpPlanar.IntegerRoots.root426 line 2429
1477. lemma OAI.SharpPlanar.IntegerRoots.root426_contains line 2430
1478. def OAI.SharpPlanar.IntegerRoots.mid427 line 2433
1479. lemma OAI.SharpPlanar.IntegerRoots.mid427_contains line 2434
1480. def OAI.SharpPlanar.IntegerRoots.root427 line 2435
1481. lemma OAI.SharpPlanar.IntegerRoots.root427_contains line 2436
1482. def OAI.SharpPlanar.IntegerRoots.root428 line 2439
1483. lemma OAI.SharpPlanar.IntegerRoots.root428_contains line 2440
1484. def OAI.SharpPlanar.IntegerRoots.mid429 line 2443
1485. lemma OAI.SharpPlanar.IntegerRoots.mid429_contains line 2444
1486. def OAI.SharpPlanar.IntegerRoots.root429 line 2445
1487. lemma OAI.SharpPlanar.IntegerRoots.root429_contains line 2446
1488. def OAI.SharpPlanar.IntegerRoots.root430 line 2449
1489. lemma OAI.SharpPlanar.IntegerRoots.root430_contains line 2450
1490. def OAI.SharpPlanar.IntegerRoots.mid431 line 2453
1491. lemma OAI.SharpPlanar.IntegerRoots.mid431_contains line 2454
1492. def OAI.SharpPlanar.IntegerRoots.root431 line 2455
1493. lemma OAI.SharpPlanar.IntegerRoots.root431_contains line 2456
1494. def OAI.SharpPlanar.IntegerRoots.root432 line 2459
1495. lemma OAI.SharpPlanar.IntegerRoots.root432_contains line 2460
1496. def OAI.SharpPlanar.IntegerRoots.mid433 line 2463
1497. lemma OAI.SharpPlanar.IntegerRoots.mid433_contains line 2464
1498. def OAI.SharpPlanar.IntegerRoots.root433 line 2465
1499. lemma OAI.SharpPlanar.IntegerRoots.root433_contains line 2466
1500. def OAI.SharpPlanar.IntegerRoots.root434 line 2469
1501. lemma OAI.SharpPlanar.IntegerRoots.root434_contains line 2470
1502. def OAI.SharpPlanar.IntegerRoots.mid435 line 2473
1503. lemma OAI.SharpPlanar.IntegerRoots.mid435_contains line 2474
1504. def OAI.SharpPlanar.IntegerRoots.root435 line 2475
1505. lemma OAI.SharpPlanar.IntegerRoots.root435_contains line 2476
1506. def OAI.SharpPlanar.IntegerRoots.root436 line 2479
1507. lemma OAI.SharpPlanar.IntegerRoots.root436_contains line 2480
1508. def OAI.SharpPlanar.IntegerRoots.mid437 line 2483
1509. lemma OAI.SharpPlanar.IntegerRoots.mid437_contains line 2484
1510. def OAI.SharpPlanar.IntegerRoots.root437 line 2485
1511. lemma OAI.SharpPlanar.IntegerRoots.root437_contains line 2486
1512. def OAI.SharpPlanar.IntegerRoots.root438 line 2489
1513. lemma OAI.SharpPlanar.IntegerRoots.root438_contains line 2490
1514. def OAI.SharpPlanar.IntegerRoots.mid439 line 2493
1515. lemma OAI.SharpPlanar.IntegerRoots.mid439_contains line 2494
1516. def OAI.SharpPlanar.IntegerRoots.root439 line 2495
1517. lemma OAI.SharpPlanar.IntegerRoots.root439_contains line 2496
1518. def OAI.SharpPlanar.IntegerRoots.root440 line 2499
1519. lemma OAI.SharpPlanar.IntegerRoots.root440_contains line 2500
1520. def OAI.SharpPlanar.IntegerRoots.mid441 line 2503
1521. lemma OAI.SharpPlanar.IntegerRoots.mid441_contains line 2504
1522. def OAI.SharpPlanar.IntegerRoots.root441 line 2505
1523. lemma OAI.SharpPlanar.IntegerRoots.root441_contains line 2506
1524. def OAI.SharpPlanar.IntegerRoots.root442 line 2509
1525. lemma OAI.SharpPlanar.IntegerRoots.root442_contains line 2510
1526. def OAI.SharpPlanar.IntegerRoots.mid443 line 2513
1527. lemma OAI.SharpPlanar.IntegerRoots.mid443_contains line 2514
1528. def OAI.SharpPlanar.IntegerRoots.root443 line 2515
1529. lemma OAI.SharpPlanar.IntegerRoots.root443_contains line 2516
1530. def OAI.SharpPlanar.IntegerRoots.root444 line 2519
1531. lemma OAI.SharpPlanar.IntegerRoots.root444_contains line 2520
1532. def OAI.SharpPlanar.IntegerRoots.mid445 line 2523
1533. lemma OAI.SharpPlanar.IntegerRoots.mid445_contains line 2524
1534. def OAI.SharpPlanar.IntegerRoots.root445 line 2525
1535. lemma OAI.SharpPlanar.IntegerRoots.root445_contains line 2526
1536. def OAI.SharpPlanar.IntegerRoots.root446 line 2529
1537. lemma OAI.SharpPlanar.IntegerRoots.root446_contains line 2530
1538. def OAI.SharpPlanar.IntegerRoots.mid447 line 2533
1539. lemma OAI.SharpPlanar.IntegerRoots.mid447_contains line 2534
1540. def OAI.SharpPlanar.IntegerRoots.root447 line 2535
1541. lemma OAI.SharpPlanar.IntegerRoots.root447_contains line 2536
1542. def OAI.SharpPlanar.IntegerRoots.root448 line 2539
1543. lemma OAI.SharpPlanar.IntegerRoots.root448_contains line 2540
1544. def OAI.SharpPlanar.IntegerRoots.mid449 line 2543
1545. lemma OAI.SharpPlanar.IntegerRoots.mid449_contains line 2544
1546. def OAI.SharpPlanar.IntegerRoots.root449 line 2545
1547. lemma OAI.SharpPlanar.IntegerRoots.root449_contains line 2546
1548. def OAI.SharpPlanar.IntegerRoots.root450 line 2549
1549. lemma OAI.SharpPlanar.IntegerRoots.root450_contains line 2550
1550. def OAI.SharpPlanar.IntegerRoots.mid451 line 2553
1551. lemma OAI.SharpPlanar.IntegerRoots.mid451_contains line 2554
1552. def OAI.SharpPlanar.IntegerRoots.root451 line 2555
1553. lemma OAI.SharpPlanar.IntegerRoots.root451_contains line 2556
1554. def OAI.SharpPlanar.IntegerRoots.root452 line 2559
1555. lemma OAI.SharpPlanar.IntegerRoots.root452_contains line 2560
1556. def OAI.SharpPlanar.IntegerRoots.mid453 line 2563
1557. lemma OAI.SharpPlanar.IntegerRoots.mid453_contains line 2564
1558. def OAI.SharpPlanar.IntegerRoots.root453 line 2565
1559. lemma OAI.SharpPlanar.IntegerRoots.root453_contains line 2566
1560. def OAI.SharpPlanar.IntegerRoots.root454 line 2569
1561. lemma OAI.SharpPlanar.IntegerRoots.root454_contains line 2570
1562. def OAI.SharpPlanar.IntegerRoots.mid455 line 2573
1563. lemma OAI.SharpPlanar.IntegerRoots.mid455_contains line 2574
1564. def OAI.SharpPlanar.IntegerRoots.root455 line 2575
1565. lemma OAI.SharpPlanar.IntegerRoots.root455_contains line 2576
1566. def OAI.SharpPlanar.IntegerRoots.root456 line 2579
1567. lemma OAI.SharpPlanar.IntegerRoots.root456_contains line 2580
1568. def OAI.SharpPlanar.IntegerRoots.mid457 line 2583
1569. lemma OAI.SharpPlanar.IntegerRoots.mid457_contains line 2584
1570. def OAI.SharpPlanar.IntegerRoots.root457 line 2585
1571. lemma OAI.SharpPlanar.IntegerRoots.root457_contains line 2586
1572. def OAI.SharpPlanar.IntegerRoots.root458 line 2589
1573. lemma OAI.SharpPlanar.IntegerRoots.root458_contains line 2590
1574. def OAI.SharpPlanar.IntegerRoots.mid459 line 2593
1575. lemma OAI.SharpPlanar.IntegerRoots.mid459_contains line 2594
1576. def OAI.SharpPlanar.IntegerRoots.root459 line 2595
1577. lemma OAI.SharpPlanar.IntegerRoots.root459_contains line 2596
1578. def OAI.SharpPlanar.IntegerRoots.root460 line 2599
1579. lemma OAI.SharpPlanar.IntegerRoots.root460_contains line 2600
1580. def OAI.SharpPlanar.IntegerRoots.mid461 line 2603
1581. lemma OAI.SharpPlanar.IntegerRoots.mid461_contains line 2604
1582. def OAI.SharpPlanar.IntegerRoots.root461 line 2605
1583. lemma OAI.SharpPlanar.IntegerRoots.root461_contains line 2606
1584. def OAI.SharpPlanar.IntegerRoots.root462 line 2609
1585. lemma OAI.SharpPlanar.IntegerRoots.root462_contains line 2610
1586. def OAI.SharpPlanar.IntegerRoots.mid463 line 2613
1587. lemma OAI.SharpPlanar.IntegerRoots.mid463_contains line 2614
1588. def OAI.SharpPlanar.IntegerRoots.root463 line 2615
1589. lemma OAI.SharpPlanar.IntegerRoots.root463_contains line 2616
1590. def OAI.SharpPlanar.IntegerRoots.root464 line 2619
1591. lemma OAI.SharpPlanar.IntegerRoots.root464_contains line 2620
1592. def OAI.SharpPlanar.IntegerRoots.mid465 line 2623
1593. lemma OAI.SharpPlanar.IntegerRoots.mid465_contains line 2624
1594. def OAI.SharpPlanar.IntegerRoots.root465 line 2625
1595. lemma OAI.SharpPlanar.IntegerRoots.root465_contains line 2626
1596. def OAI.SharpPlanar.IntegerRoots.root466 line 2629
1597. lemma OAI.SharpPlanar.IntegerRoots.root466_contains line 2630
1598. def OAI.SharpPlanar.IntegerRoots.mid467 line 2633
1599. lemma OAI.SharpPlanar.IntegerRoots.mid467_contains line 2634
1600. def OAI.SharpPlanar.IntegerRoots.root467 line 2635
1601. lemma OAI.SharpPlanar.IntegerRoots.root467_contains line 2636
1602. def OAI.SharpPlanar.IntegerRoots.root468 line 2639
1603. lemma OAI.SharpPlanar.IntegerRoots.root468_contains line 2640
1604. def OAI.SharpPlanar.IntegerRoots.mid469 line 2643
1605. lemma OAI.SharpPlanar.IntegerRoots.mid469_contains line 2644
1606. def OAI.SharpPlanar.IntegerRoots.root469 line 2645
1607. lemma OAI.SharpPlanar.IntegerRoots.root469_contains line 2646
1608. def OAI.SharpPlanar.IntegerRoots.root470 line 2649
1609. lemma OAI.SharpPlanar.IntegerRoots.root470_contains line 2650
1610. def OAI.SharpPlanar.IntegerRoots.mid471 line 2653
1611. lemma OAI.SharpPlanar.IntegerRoots.mid471_contains line 2654
1612. def OAI.SharpPlanar.IntegerRoots.root471 line 2655
1613. lemma OAI.SharpPlanar.IntegerRoots.root471_contains line 2656
1614. def OAI.SharpPlanar.IntegerRoots.root472 line 2659
1615. lemma OAI.SharpPlanar.IntegerRoots.root472_contains line 2660
1616. def OAI.SharpPlanar.IntegerRoots.mid473 line 2663
1617. lemma OAI.SharpPlanar.IntegerRoots.mid473_contains line 2664
1618. def OAI.SharpPlanar.IntegerRoots.root473 line 2665
1619. lemma OAI.SharpPlanar.IntegerRoots.root473_contains line 2666
1620. def OAI.SharpPlanar.IntegerRoots.root474 line 2669
1621. lemma OAI.SharpPlanar.IntegerRoots.root474_contains line 2670
1622. def OAI.SharpPlanar.IntegerRoots.mid475 line 2673
1623. lemma OAI.SharpPlanar.IntegerRoots.mid475_contains line 2674
1624. def OAI.SharpPlanar.IntegerRoots.root475 line 2675
1625. lemma OAI.SharpPlanar.IntegerRoots.root475_contains line 2676
1626. def OAI.SharpPlanar.IntegerRoots.root476 line 2679
1627. lemma OAI.SharpPlanar.IntegerRoots.root476_contains line 2680
1628. def OAI.SharpPlanar.IntegerRoots.mid477 line 2683
1629. lemma OAI.SharpPlanar.IntegerRoots.mid477_contains line 2684
1630. def OAI.SharpPlanar.IntegerRoots.root477 line 2685
1631. lemma OAI.SharpPlanar.IntegerRoots.root477_contains line 2686
1632. def OAI.SharpPlanar.IntegerRoots.root478 line 2689
1633. lemma OAI.SharpPlanar.IntegerRoots.root478_contains line 2690
1634. def OAI.SharpPlanar.IntegerRoots.mid479 line 2693
1635. lemma OAI.SharpPlanar.IntegerRoots.mid479_contains line 2694
1636. def OAI.SharpPlanar.IntegerRoots.root479 line 2695
1637. lemma OAI.SharpPlanar.IntegerRoots.root479_contains line 2696
1638. def OAI.SharpPlanar.IntegerRoots.root480 line 2699
1639. lemma OAI.SharpPlanar.IntegerRoots.root480_contains line 2700
1640. def OAI.SharpPlanar.IntegerRoots.mid481 line 2703
1641. lemma OAI.SharpPlanar.IntegerRoots.mid481_contains line 2704
1642. def OAI.SharpPlanar.IntegerRoots.root481 line 2705
1643. lemma OAI.SharpPlanar.IntegerRoots.root481_contains line 2706
1644. def OAI.SharpPlanar.IntegerRoots.root482 line 2709
1645. lemma OAI.SharpPlanar.IntegerRoots.root482_contains line 2710
1646. def OAI.SharpPlanar.IntegerRoots.mid483 line 2713
1647. lemma OAI.SharpPlanar.IntegerRoots.mid483_contains line 2714
1648. def OAI.SharpPlanar.IntegerRoots.root483 line 2715
1649. lemma OAI.SharpPlanar.IntegerRoots.root483_contains line 2716
1650. def OAI.SharpPlanar.IntegerRoots.root484 line 2719
1651. lemma OAI.SharpPlanar.IntegerRoots.root484_contains line 2720
1652. def OAI.SharpPlanar.IntegerRoots.mid485 line 2723
1653. lemma OAI.SharpPlanar.IntegerRoots.mid485_contains line 2724
1654. def OAI.SharpPlanar.IntegerRoots.root485 line 2725
1655. lemma OAI.SharpPlanar.IntegerRoots.root485_contains line 2726
1656. def OAI.SharpPlanar.IntegerRoots.root486 line 2729
1657. lemma OAI.SharpPlanar.IntegerRoots.root486_contains line 2730
1658. def OAI.SharpPlanar.IntegerRoots.mid487 line 2733
1659. lemma OAI.SharpPlanar.IntegerRoots.mid487_contains line 2734
1660. def OAI.SharpPlanar.IntegerRoots.root487 line 2735
1661. lemma OAI.SharpPlanar.IntegerRoots.root487_contains line 2736
1662. def OAI.SharpPlanar.IntegerRoots.root488 line 2739
1663. lemma OAI.SharpPlanar.IntegerRoots.root488_contains line 2740
1664. def OAI.SharpPlanar.IntegerRoots.mid489 line 2743
1665. lemma OAI.SharpPlanar.IntegerRoots.mid489_contains line 2744
1666. def OAI.SharpPlanar.IntegerRoots.root489 line 2745
1667. lemma OAI.SharpPlanar.IntegerRoots.root489_contains line 2746
1668. def OAI.SharpPlanar.IntegerRoots.root490 line 2749
1669. lemma OAI.SharpPlanar.IntegerRoots.root490_contains line 2750
1670. def OAI.SharpPlanar.IntegerRoots.mid491 line 2753
1671. lemma OAI.SharpPlanar.IntegerRoots.mid491_contains line 2754
1672. def OAI.SharpPlanar.IntegerRoots.root491 line 2755
1673. lemma OAI.SharpPlanar.IntegerRoots.root491_contains line 2756
1674. def OAI.SharpPlanar.IntegerRoots.root492 line 2759
1675. lemma OAI.SharpPlanar.IntegerRoots.root492_contains line 2760
1676. def OAI.SharpPlanar.IntegerRoots.mid493 line 2763
1677. lemma OAI.SharpPlanar.IntegerRoots.mid493_contains line 2764
1678. def OAI.SharpPlanar.IntegerRoots.root493 line 2765
1679. lemma OAI.SharpPlanar.IntegerRoots.root493_contains line 2766
1680. def OAI.SharpPlanar.IntegerRoots.root494 line 2769
1681. lemma OAI.SharpPlanar.IntegerRoots.root494_contains line 2770
1682. def OAI.SharpPlanar.IntegerRoots.mid495 line 2773
1683. lemma OAI.SharpPlanar.IntegerRoots.mid495_contains line 2774
1684. def OAI.SharpPlanar.IntegerRoots.root495 line 2775
1685. lemma OAI.SharpPlanar.IntegerRoots.root495_contains line 2776
1686. def OAI.SharpPlanar.IntegerRoots.root496 line 2779
1687. lemma OAI.SharpPlanar.IntegerRoots.root496_contains line 2780
1688. def OAI.SharpPlanar.IntegerRoots.mid497 line 2783
1689. lemma OAI.SharpPlanar.IntegerRoots.mid497_contains line 2784
1690. def OAI.SharpPlanar.IntegerRoots.root497 line 2785
1691. lemma OAI.SharpPlanar.IntegerRoots.root497_contains line 2786
1692. def OAI.SharpPlanar.IntegerRoots.root498 line 2789
1693. lemma OAI.SharpPlanar.IntegerRoots.root498_contains line 2790
1694. def OAI.SharpPlanar.IntegerRoots.mid499 line 2793
1695. lemma OAI.SharpPlanar.IntegerRoots.mid499_contains line 2794
1696. def OAI.SharpPlanar.IntegerRoots.root499 line 2795
1697. lemma OAI.SharpPlanar.IntegerRoots.root499_contains line 2796
1698. def OAI.SharpPlanar.IntegerRoots.root500 line 2799
1699. lemma OAI.SharpPlanar.IntegerRoots.root500_contains line 2800
1700. def OAI.SharpPlanar.IntegerRoots.mid501 line 2803
1701. lemma OAI.SharpPlanar.IntegerRoots.mid501_contains line 2804
1702. def OAI.SharpPlanar.IntegerRoots.root501 line 2805
1703. lemma OAI.SharpPlanar.IntegerRoots.root501_contains line 2806
1704. def OAI.SharpPlanar.IntegerRoots.root502 line 2809
1705. lemma OAI.SharpPlanar.IntegerRoots.root502_contains line 2810
1706. def OAI.SharpPlanar.IntegerRoots.mid503 line 2813
1707. lemma OAI.SharpPlanar.IntegerRoots.mid503_contains line 2814
1708. def OAI.SharpPlanar.IntegerRoots.root503 line 2815
1709. lemma OAI.SharpPlanar.IntegerRoots.root503_contains line 2816
1710. def OAI.SharpPlanar.IntegerRoots.root504 line 2819
1711. lemma OAI.SharpPlanar.IntegerRoots.root504_contains line 2820
1712. def OAI.SharpPlanar.IntegerRoots.mid505 line 2823
1713. lemma OAI.SharpPlanar.IntegerRoots.mid505_contains line 2824
1714. def OAI.SharpPlanar.IntegerRoots.root505 line 2825
1715. lemma OAI.SharpPlanar.IntegerRoots.root505_contains line 2826
1716. def OAI.SharpPlanar.IntegerRoots.root506 line 2829
1717. lemma OAI.SharpPlanar.IntegerRoots.root506_contains line 2830
1718. def OAI.SharpPlanar.IntegerRoots.mid507 line 2833
1719. lemma OAI.SharpPlanar.IntegerRoots.mid507_contains line 2834
1720. def OAI.SharpPlanar.IntegerRoots.root507 line 2835
1721. lemma OAI.SharpPlanar.IntegerRoots.root507_contains line 2836
1722. def OAI.SharpPlanar.IntegerRoots.root508 line 2839
1723. lemma OAI.SharpPlanar.IntegerRoots.root508_contains line 2840
1724. def OAI.SharpPlanar.IntegerRoots.mid509 line 2843
1725. lemma OAI.SharpPlanar.IntegerRoots.mid509_contains line 2844
1726. def OAI.SharpPlanar.IntegerRoots.root509 line 2845
1727. lemma OAI.SharpPlanar.IntegerRoots.root509_contains line 2846
1728. def OAI.SharpPlanar.IntegerRoots.root510 line 2849
1729. lemma OAI.SharpPlanar.IntegerRoots.root510_contains line 2850
1730. def OAI.SharpPlanar.IntegerRoots.mid511 line 2853
1731. lemma OAI.SharpPlanar.IntegerRoots.mid511_contains line 2854
1732. def OAI.SharpPlanar.IntegerRoots.root511 line 2855
1733. lemma OAI.SharpPlanar.IntegerRoots.root511_contains line 2856
1734. def OAI.SharpPlanar.IntegerRoots.root512 line 2859
1735. lemma OAI.SharpPlanar.IntegerRoots.root512_contains line 2860
1736. def OAI.SharpPlanar.IntegerRoots.mid513 line 2863
1737. lemma OAI.SharpPlanar.IntegerRoots.mid513_contains line 2864
1738. def OAI.SharpPlanar.IntegerRoots.root513 line 2865
1739. lemma OAI.SharpPlanar.IntegerRoots.root513_contains line 2866
1740. def OAI.SharpPlanar.IntegerRoots.root514 line 2869
1741. lemma OAI.SharpPlanar.IntegerRoots.root514_contains line 2870
1742. def OAI.SharpPlanar.IntegerRoots.mid515 line 2873
1743. lemma OAI.SharpPlanar.IntegerRoots.mid515_contains line 2874
1744. def OAI.SharpPlanar.IntegerRoots.root515 line 2875
1745. lemma OAI.SharpPlanar.IntegerRoots.root515_contains line 2876
1746. def OAI.SharpPlanar.IntegerRoots.root516 line 2879
1747. lemma OAI.SharpPlanar.IntegerRoots.root516_contains line 2880
1748. def OAI.SharpPlanar.IntegerRoots.mid517 line 2883
1749. lemma OAI.SharpPlanar.IntegerRoots.mid517_contains line 2884
1750. def OAI.SharpPlanar.IntegerRoots.root517 line 2885
1751. lemma OAI.SharpPlanar.IntegerRoots.root517_contains line 2886
1752. def OAI.SharpPlanar.IntegerRoots.root518 line 2889
1753. lemma OAI.SharpPlanar.IntegerRoots.root518_contains line 2890
1754. def OAI.SharpPlanar.IntegerRoots.mid519 line 2893
1755. lemma OAI.SharpPlanar.IntegerRoots.mid519_contains line 2894
1756. def OAI.SharpPlanar.IntegerRoots.root519 line 2895
1757. lemma OAI.SharpPlanar.IntegerRoots.root519_contains line 2896
1758. def OAI.SharpPlanar.IntegerRoots.root520 line 2899
1759. lemma OAI.SharpPlanar.IntegerRoots.root520_contains line 2900
1760. def OAI.SharpPlanar.IntegerRoots.mid521 line 2903
1761. lemma OAI.SharpPlanar.IntegerRoots.mid521_contains line 2904
1762. def OAI.SharpPlanar.IntegerRoots.root521 line 2905
1763. lemma OAI.SharpPlanar.IntegerRoots.root521_contains line 2906
1764. def OAI.SharpPlanar.IntegerRoots.root522 line 2909
1765. lemma OAI.SharpPlanar.IntegerRoots.root522_contains line 2910
1766. def OAI.SharpPlanar.IntegerRoots.mid523 line 2913
1767. lemma OAI.SharpPlanar.IntegerRoots.mid523_contains line 2914
1768. def OAI.SharpPlanar.IntegerRoots.root523 line 2915
1769. lemma OAI.SharpPlanar.IntegerRoots.root523_contains line 2916
1770. def OAI.SharpPlanar.IntegerRoots.root524 line 2919
1771. lemma OAI.SharpPlanar.IntegerRoots.root524_contains line 2920
1772. def OAI.SharpPlanar.IntegerRoots.mid525 line 2923
1773. lemma OAI.SharpPlanar.IntegerRoots.mid525_contains line 2924
1774. def OAI.SharpPlanar.IntegerRoots.root525 line 2925
1775. lemma OAI.SharpPlanar.IntegerRoots.root525_contains line 2926
1776. def OAI.SharpPlanar.IntegerRoots.root526 line 2929
1777. lemma OAI.SharpPlanar.IntegerRoots.root526_contains line 2930
1778. def OAI.SharpPlanar.IntegerRoots.mid527 line 2933
1779. lemma OAI.SharpPlanar.IntegerRoots.mid527_contains line 2934
1780. def OAI.SharpPlanar.IntegerRoots.root527 line 2935
1781. lemma OAI.SharpPlanar.IntegerRoots.root527_contains line 2936
1782. def OAI.SharpPlanar.IntegerRoots.root528 line 2939
1783. lemma OAI.SharpPlanar.IntegerRoots.root528_contains line 2940
1784. def OAI.SharpPlanar.IntegerRoots.mid529 line 2943
1785. lemma OAI.SharpPlanar.IntegerRoots.mid529_contains line 2944
1786. def OAI.SharpPlanar.IntegerRoots.root529 line 2945
1787. lemma OAI.SharpPlanar.IntegerRoots.root529_contains line 2946
1788. def OAI.SharpPlanar.IntegerRoots.root530 line 2949
1789. lemma OAI.SharpPlanar.IntegerRoots.root530_contains line 2950
1790. def OAI.SharpPlanar.IntegerRoots.mid531 line 2953
1791. lemma OAI.SharpPlanar.IntegerRoots.mid531_contains line 2954
1792. def OAI.SharpPlanar.IntegerRoots.root531 line 2955
1793. lemma OAI.SharpPlanar.IntegerRoots.root531_contains line 2956
1794. def OAI.SharpPlanar.IntegerRoots.root532 line 2959
1795. lemma OAI.SharpPlanar.IntegerRoots.root532_contains line 2960
1796. def OAI.SharpPlanar.IntegerRoots.mid533 line 2963
1797. lemma OAI.SharpPlanar.IntegerRoots.mid533_contains line 2964
1798. def OAI.SharpPlanar.IntegerRoots.root533 line 2965
1799. lemma OAI.SharpPlanar.IntegerRoots.root533_contains line 2966
1800. def OAI.SharpPlanar.IntegerRoots.root534 line 2969
1801. lemma OAI.SharpPlanar.IntegerRoots.root534_contains line 2970
1802. def OAI.SharpPlanar.IntegerRoots.mid535 line 2973
1803. lemma OAI.SharpPlanar.IntegerRoots.mid535_contains line 2974
1804. def OAI.SharpPlanar.IntegerRoots.root535 line 2975
1805. lemma OAI.SharpPlanar.IntegerRoots.root535_contains line 2976
1806. def OAI.SharpPlanar.IntegerRoots.root536 line 2979
1807. lemma OAI.SharpPlanar.IntegerRoots.root536_contains line 2980
1808. def OAI.SharpPlanar.IntegerRoots.mid537 line 2983
1809. lemma OAI.SharpPlanar.IntegerRoots.mid537_contains line 2984
1810. def OAI.SharpPlanar.IntegerRoots.root537 line 2985
1811. lemma OAI.SharpPlanar.IntegerRoots.root537_contains line 2986
1812. def OAI.SharpPlanar.IntegerRoots.root538 line 2989
1813. lemma OAI.SharpPlanar.IntegerRoots.root538_contains line 2990
1814. def OAI.SharpPlanar.IntegerRoots.mid539 line 2993
1815. lemma OAI.SharpPlanar.IntegerRoots.mid539_contains line 2994
1816. def OAI.SharpPlanar.IntegerRoots.root539 line 2995
1817. lemma OAI.SharpPlanar.IntegerRoots.root539_contains line 2996
1818. def OAI.SharpPlanar.IntegerRoots.root540 line 2999
1819. lemma OAI.SharpPlanar.IntegerRoots.root540_contains line 3000
1820. def OAI.SharpPlanar.IntegerRoots.mid541 line 3003
1821. lemma OAI.SharpPlanar.IntegerRoots.mid541_contains line 3004
1822. def OAI.SharpPlanar.IntegerRoots.root541 line 3005
1823. lemma OAI.SharpPlanar.IntegerRoots.root541_contains line 3006
1824. def OAI.SharpPlanar.IntegerRoots.root542 line 3009
1825. lemma OAI.SharpPlanar.IntegerRoots.root542_contains line 3010
1826. def OAI.SharpPlanar.IntegerRoots.mid543 line 3013
1827. lemma OAI.SharpPlanar.IntegerRoots.mid543_contains line 3014
1828. def OAI.SharpPlanar.IntegerRoots.root543 line 3015
1829. lemma OAI.SharpPlanar.IntegerRoots.root543_contains line 3016
1830. def OAI.SharpPlanar.IntegerRoots.root544 line 3019
1831. lemma OAI.SharpPlanar.IntegerRoots.root544_contains line 3020
1832. def OAI.SharpPlanar.IntegerRoots.mid545 line 3023
1833. lemma OAI.SharpPlanar.IntegerRoots.mid545_contains line 3024
1834. def OAI.SharpPlanar.IntegerRoots.root545 line 3025
1835. lemma OAI.SharpPlanar.IntegerRoots.root545_contains line 3026
1836. def OAI.SharpPlanar.IntegerRoots.root546 line 3029
1837. lemma OAI.SharpPlanar.IntegerRoots.root546_contains line 3030
1838. def OAI.SharpPlanar.IntegerRoots.mid547 line 3033
1839. lemma OAI.SharpPlanar.IntegerRoots.mid547_contains line 3034
1840. def OAI.SharpPlanar.IntegerRoots.root547 line 3035
1841. lemma OAI.SharpPlanar.IntegerRoots.root547_contains line 3036
1842. def OAI.SharpPlanar.IntegerRoots.root548 line 3039
1843. lemma OAI.SharpPlanar.IntegerRoots.root548_contains line 3040
1844. def OAI.SharpPlanar.IntegerRoots.mid549 line 3043
1845. lemma OAI.SharpPlanar.IntegerRoots.mid549_contains line 3044
1846. def OAI.SharpPlanar.IntegerRoots.root549 line 3045
1847. lemma OAI.SharpPlanar.IntegerRoots.root549_contains line 3046
1848. def OAI.SharpPlanar.IntegerRoots.root550 line 3049
1849. lemma OAI.SharpPlanar.IntegerRoots.root550_contains line 3050
1850. def OAI.SharpPlanar.IntegerRoots.mid551 line 3053
1851. lemma OAI.SharpPlanar.IntegerRoots.mid551_contains line 3054
1852. def OAI.SharpPlanar.IntegerRoots.root551 line 3055
1853. lemma OAI.SharpPlanar.IntegerRoots.root551_contains line 3056
1854. def OAI.SharpPlanar.IntegerRoots.root552 line 3059
1855. lemma OAI.SharpPlanar.IntegerRoots.root552_contains line 3060
1856. def OAI.SharpPlanar.IntegerRoots.mid553 line 3063
1857. lemma OAI.SharpPlanar.IntegerRoots.mid553_contains line 3064
1858. def OAI.SharpPlanar.IntegerRoots.root553 line 3065
1859. lemma OAI.SharpPlanar.IntegerRoots.root553_contains line 3066
1860. def OAI.SharpPlanar.IntegerRoots.root554 line 3069
1861. lemma OAI.SharpPlanar.IntegerRoots.root554_contains line 3070
1862. def OAI.SharpPlanar.IntegerRoots.mid555 line 3073
1863. lemma OAI.SharpPlanar.IntegerRoots.mid555_contains line 3074
1864. def OAI.SharpPlanar.IntegerRoots.root555 line 3075
1865. lemma OAI.SharpPlanar.IntegerRoots.root555_contains line 3076
1866. def OAI.SharpPlanar.IntegerRoots.root556 line 3079
1867. lemma OAI.SharpPlanar.IntegerRoots.root556_contains line 3080
1868. def OAI.SharpPlanar.IntegerRoots.mid557 line 3083
1869. lemma OAI.SharpPlanar.IntegerRoots.mid557_contains line 3084
1870. def OAI.SharpPlanar.IntegerRoots.root557 line 3085
1871. lemma OAI.SharpPlanar.IntegerRoots.root557_contains line 3086
1872. def OAI.SharpPlanar.IntegerRoots.root558 line 3089
1873. lemma OAI.SharpPlanar.IntegerRoots.root558_contains line 3090
1874. def OAI.SharpPlanar.IntegerRoots.mid559 line 3093
1875. lemma OAI.SharpPlanar.IntegerRoots.mid559_contains line 3094
1876. def OAI.SharpPlanar.IntegerRoots.root559 line 3095
1877. lemma OAI.SharpPlanar.IntegerRoots.root559_contains line 3096
1878. def OAI.SharpPlanar.IntegerRoots.root560 line 3099
1879. lemma OAI.SharpPlanar.IntegerRoots.root560_contains line 3100
1880. def OAI.SharpPlanar.IntegerRoots.mid561 line 3103
1881. lemma OAI.SharpPlanar.IntegerRoots.mid561_contains line 3104
1882. def OAI.SharpPlanar.IntegerRoots.root561 line 3105
1883. lemma OAI.SharpPlanar.IntegerRoots.root561_contains line 3106
1884. def OAI.SharpPlanar.IntegerRoots.root562 line 3109
1885. lemma OAI.SharpPlanar.IntegerRoots.root562_contains line 3110
1886. def OAI.SharpPlanar.IntegerRoots.mid563 line 3113
1887. lemma OAI.SharpPlanar.IntegerRoots.mid563_contains line 3114
1888. def OAI.SharpPlanar.IntegerRoots.root563 line 3115
1889. lemma OAI.SharpPlanar.IntegerRoots.root563_contains line 3116
1890. def OAI.SharpPlanar.IntegerRoots.root564 line 3119
1891. lemma OAI.SharpPlanar.IntegerRoots.root564_contains line 3120
1892. def OAI.SharpPlanar.IntegerRoots.mid565 line 3123
1893. lemma OAI.SharpPlanar.IntegerRoots.mid565_contains line 3124
1894. def OAI.SharpPlanar.IntegerRoots.root565 line 3125
1895. lemma OAI.SharpPlanar.IntegerRoots.root565_contains line 3126
1896. def OAI.SharpPlanar.IntegerRoots.root566 line 3129
1897. lemma OAI.SharpPlanar.IntegerRoots.root566_contains line 3130
1898. def OAI.SharpPlanar.IntegerRoots.mid567 line 3133
1899. lemma OAI.SharpPlanar.IntegerRoots.mid567_contains line 3134
1900. def OAI.SharpPlanar.IntegerRoots.root567 line 3135
1901. lemma OAI.SharpPlanar.IntegerRoots.root567_contains line 3136
1902. def OAI.SharpPlanar.IntegerRoots.root568 line 3139
1903. lemma OAI.SharpPlanar.IntegerRoots.root568_contains line 3140
1904. def OAI.SharpPlanar.IntegerRoots.mid569 line 3143
1905. lemma OAI.SharpPlanar.IntegerRoots.mid569_contains line 3144
1906. def OAI.SharpPlanar.IntegerRoots.root569 line 3145
1907. lemma OAI.SharpPlanar.IntegerRoots.root569_contains line 3146
1908. def OAI.SharpPlanar.IntegerRoots.root570 line 3149
1909. lemma OAI.SharpPlanar.IntegerRoots.root570_contains line 3150
1910. def OAI.SharpPlanar.IntegerRoots.mid571 line 3153
1911. lemma OAI.SharpPlanar.IntegerRoots.mid571_contains line 3154
1912. def OAI.SharpPlanar.IntegerRoots.root571 line 3155
1913. lemma OAI.SharpPlanar.IntegerRoots.root571_contains line 3156
1914. def OAI.SharpPlanar.IntegerRoots.root572 line 3159
1915. lemma OAI.SharpPlanar.IntegerRoots.root572_contains line 3160
1916. def OAI.SharpPlanar.IntegerRoots.mid573 line 3163
1917. lemma OAI.SharpPlanar.IntegerRoots.mid573_contains line 3164
1918. def OAI.SharpPlanar.IntegerRoots.root573 line 3165
1919. lemma OAI.SharpPlanar.IntegerRoots.root573_contains line 3166
1920. def OAI.SharpPlanar.IntegerRoots.root574 line 3169
1921. lemma OAI.SharpPlanar.IntegerRoots.root574_contains line 3170
1922. def OAI.SharpPlanar.IntegerRoots.mid575 line 3173
1923. lemma OAI.SharpPlanar.IntegerRoots.mid575_contains line 3174
1924. def OAI.SharpPlanar.IntegerRoots.root575 line 3175
1925. lemma OAI.SharpPlanar.IntegerRoots.root575_contains line 3176
1926. def OAI.SharpPlanar.IntegerRoots.root576 line 3179
1927. lemma OAI.SharpPlanar.IntegerRoots.root576_contains line 3180
1928. def OAI.SharpPlanar.IntegerRoots.mid577 line 3183
1929. lemma OAI.SharpPlanar.IntegerRoots.mid577_contains line 3184
1930. def OAI.SharpPlanar.IntegerRoots.root577 line 3185
1931. lemma OAI.SharpPlanar.IntegerRoots.root577_contains line 3186
1932. def OAI.SharpPlanar.IntegerRoots.root578 line 3189
1933. lemma OAI.SharpPlanar.IntegerRoots.root578_contains line 3190
1934. def OAI.SharpPlanar.IntegerRoots.mid579 line 3193
1935. lemma OAI.SharpPlanar.IntegerRoots.mid579_contains line 3194
1936. def OAI.SharpPlanar.IntegerRoots.root579 line 3195
1937. lemma OAI.SharpPlanar.IntegerRoots.root579_contains line 3196
1938. def OAI.SharpPlanar.IntegerRoots.root580 line 3199
1939. lemma OAI.SharpPlanar.IntegerRoots.root580_contains line 3200
1940. def OAI.SharpPlanar.IntegerRoots.mid581 line 3203
1941. lemma OAI.SharpPlanar.IntegerRoots.mid581_contains line 3204
1942. def OAI.SharpPlanar.IntegerRoots.root581 line 3205
1943. lemma OAI.SharpPlanar.IntegerRoots.root581_contains line 3206
1944. def OAI.SharpPlanar.IntegerRoots.root582 line 3209
1945. lemma OAI.SharpPlanar.IntegerRoots.root582_contains line 3210
1946. def OAI.SharpPlanar.IntegerRoots.mid583 line 3213
1947. lemma OAI.SharpPlanar.IntegerRoots.mid583_contains line 3214
1948. def OAI.SharpPlanar.IntegerRoots.root583 line 3215
1949. lemma OAI.SharpPlanar.IntegerRoots.root583_contains line 3216
1950. def OAI.SharpPlanar.IntegerRoots.root584 line 3219
1951. lemma OAI.SharpPlanar.IntegerRoots.root584_contains line 3220
1952. def OAI.SharpPlanar.IntegerRoots.mid585 line 3223
1953. lemma OAI.SharpPlanar.IntegerRoots.mid585_contains line 3224
1954. def OAI.SharpPlanar.IntegerRoots.root585 line 3225
1955. lemma OAI.SharpPlanar.IntegerRoots.root585_contains line 3226
1956. def OAI.SharpPlanar.IntegerRoots.root586 line 3229
1957. lemma OAI.SharpPlanar.IntegerRoots.root586_contains line 3230
1958. def OAI.SharpPlanar.IntegerRoots.mid587 line 3233
1959. lemma OAI.SharpPlanar.IntegerRoots.mid587_contains line 3234
1960. def OAI.SharpPlanar.IntegerRoots.root587 line 3235
1961. lemma OAI.SharpPlanar.IntegerRoots.root587_contains line 3236
1962. def OAI.SharpPlanar.IntegerRoots.root588 line 3239
1963. lemma OAI.SharpPlanar.IntegerRoots.root588_contains line 3240
1964. def OAI.SharpPlanar.IntegerRoots.mid589 line 3243
1965. lemma OAI.SharpPlanar.IntegerRoots.mid589_contains line 3244
1966. def OAI.SharpPlanar.IntegerRoots.root589 line 3245
1967. lemma OAI.SharpPlanar.IntegerRoots.root589_contains line 3246
1968. def OAI.SharpPlanar.IntegerRoots.root590 line 3249
1969. lemma OAI.SharpPlanar.IntegerRoots.root590_contains line 3250
1970. def OAI.SharpPlanar.IntegerRoots.mid591 line 3253
1971. lemma OAI.SharpPlanar.IntegerRoots.mid591_contains line 3254
1972. def OAI.SharpPlanar.IntegerRoots.root591 line 3255
1973. lemma OAI.SharpPlanar.IntegerRoots.root591_contains line 3256
1974. def OAI.SharpPlanar.IntegerRoots.root592 line 3259
1975. lemma OAI.SharpPlanar.IntegerRoots.root592_contains line 3260
1976. def OAI.SharpPlanar.IntegerRoots.mid593 line 3263
1977. lemma OAI.SharpPlanar.IntegerRoots.mid593_contains line 3264
1978. def OAI.SharpPlanar.IntegerRoots.root593 line 3265
1979. lemma OAI.SharpPlanar.IntegerRoots.root593_contains line 3266
1980. def OAI.SharpPlanar.IntegerRoots.root594 line 3269
1981. lemma OAI.SharpPlanar.IntegerRoots.root594_contains line 3270
1982. def OAI.SharpPlanar.IntegerRoots.mid595 line 3273
1983. lemma OAI.SharpPlanar.IntegerRoots.mid595_contains line 3274
1984. def OAI.SharpPlanar.IntegerRoots.root595 line 3275
1985. lemma OAI.SharpPlanar.IntegerRoots.root595_contains line 3276
1986. def OAI.SharpPlanar.IntegerRoots.root596 line 3279
1987. lemma OAI.SharpPlanar.IntegerRoots.root596_contains line 3280
1988. def OAI.SharpPlanar.IntegerRoots.mid597 line 3283
1989. lemma OAI.SharpPlanar.IntegerRoots.mid597_contains line 3284
1990. def OAI.SharpPlanar.IntegerRoots.root597 line 3285
1991. lemma OAI.SharpPlanar.IntegerRoots.root597_contains line 3286
1992. def OAI.SharpPlanar.IntegerRoots.root598 line 3289
1993. lemma OAI.SharpPlanar.IntegerRoots.root598_contains line 3290
1994. def OAI.SharpPlanar.IntegerRoots.mid599 line 3293
1995. lemma OAI.SharpPlanar.IntegerRoots.mid599_contains line 3294
1996. def OAI.SharpPlanar.IntegerRoots.root599 line 3295
1997. lemma OAI.SharpPlanar.IntegerRoots.root599_contains line 3296
1998. def OAI.SharpPlanar.IntegerRoots.root600 line 3299
1999. lemma OAI.SharpPlanar.IntegerRoots.root600_contains line 3300
2000. def OAI.SharpPlanar.IntegerRoots.mid601 line 3303
2001. lemma OAI.SharpPlanar.IntegerRoots.mid601_contains line 3304
2002. def OAI.SharpPlanar.IntegerRoots.root601 line 3305
2003. lemma OAI.SharpPlanar.IntegerRoots.root601_contains line 3306
2004. def OAI.SharpPlanar.IntegerRoots.root602 line 3309
2005. lemma OAI.SharpPlanar.IntegerRoots.root602_contains line 3310
2006. def OAI.SharpPlanar.IntegerRoots.mid603 line 3313
2007. lemma OAI.SharpPlanar.IntegerRoots.mid603_contains line 3314
2008. def OAI.SharpPlanar.IntegerRoots.root603 line 3315
2009. lemma OAI.SharpPlanar.IntegerRoots.root603_contains line 3316
2010. def OAI.SharpPlanar.IntegerRoots.root604 line 3319
2011. lemma OAI.SharpPlanar.IntegerRoots.root604_contains line 3320
2012. def OAI.SharpPlanar.IntegerRoots.mid605 line 3323
2013. lemma OAI.SharpPlanar.IntegerRoots.mid605_contains line 3324
2014. def OAI.SharpPlanar.IntegerRoots.root605 line 3325
2015. lemma OAI.SharpPlanar.IntegerRoots.root605_contains line 3326
2016. def OAI.SharpPlanar.IntegerRoots.root606 line 3329
2017. lemma OAI.SharpPlanar.IntegerRoots.root606_contains line 3330
2018. def OAI.SharpPlanar.IntegerRoots.mid607 line 3333
2019. lemma OAI.SharpPlanar.IntegerRoots.mid607_contains line 3334
2020. def OAI.SharpPlanar.IntegerRoots.root607 line 3335
2021. lemma OAI.SharpPlanar.IntegerRoots.root607_contains line 3336
2022. def OAI.SharpPlanar.IntegerRoots.root608 line 3339
2023. lemma OAI.SharpPlanar.IntegerRoots.root608_contains line 3340
2024. def OAI.SharpPlanar.IntegerRoots.mid609 line 3343
2025. lemma OAI.SharpPlanar.IntegerRoots.mid609_contains line 3344
2026. def OAI.SharpPlanar.IntegerRoots.root609 line 3345
2027. lemma OAI.SharpPlanar.IntegerRoots.root609_contains line 3346
2028. def OAI.SharpPlanar.IntegerRoots.root610 line 3349
2029. lemma OAI.SharpPlanar.IntegerRoots.root610_contains line 3350
2030. def OAI.SharpPlanar.IntegerRoots.mid611 line 3353
2031. lemma OAI.SharpPlanar.IntegerRoots.mid611_contains line 3354
2032. def OAI.SharpPlanar.IntegerRoots.root611 line 3355
2033. lemma OAI.SharpPlanar.IntegerRoots.root611_contains line 3356
2034. def OAI.SharpPlanar.IntegerRoots.root612 line 3359
2035. lemma OAI.SharpPlanar.IntegerRoots.root612_contains line 3360
2036. def OAI.SharpPlanar.IntegerRoots.mid613 line 3363
2037. lemma OAI.SharpPlanar.IntegerRoots.mid613_contains line 3364
2038. def OAI.SharpPlanar.IntegerRoots.root613 line 3365
2039. lemma OAI.SharpPlanar.IntegerRoots.root613_contains line 3366
2040. def OAI.SharpPlanar.IntegerRoots.root614 line 3369
2041. lemma OAI.SharpPlanar.IntegerRoots.root614_contains line 3370
2042. def OAI.SharpPlanar.IntegerRoots.mid615 line 3373
2043. lemma OAI.SharpPlanar.IntegerRoots.mid615_contains line 3374
2044. def OAI.SharpPlanar.IntegerRoots.root615 line 3375
2045. lemma OAI.SharpPlanar.IntegerRoots.root615_contains line 3376
2046. def OAI.SharpPlanar.IntegerRoots.root616 line 3379
2047. lemma OAI.SharpPlanar.IntegerRoots.root616_contains line 3380
2048. def OAI.SharpPlanar.IntegerRoots.mid617 line 3383
2049. lemma OAI.SharpPlanar.IntegerRoots.mid617_contains line 3384
2050. def OAI.SharpPlanar.IntegerRoots.root617 line 3385
2051. lemma OAI.SharpPlanar.IntegerRoots.root617_contains line 3386
2052. def OAI.SharpPlanar.IntegerRoots.root618 line 3389
2053. lemma OAI.SharpPlanar.IntegerRoots.root618_contains line 3390
2054. def OAI.SharpPlanar.IntegerRoots.mid619 line 3393
2055. lemma OAI.SharpPlanar.IntegerRoots.mid619_contains line 3394
2056. def OAI.SharpPlanar.IntegerRoots.root619 line 3395
2057. lemma OAI.SharpPlanar.IntegerRoots.root619_contains line 3396
2058. def OAI.SharpPlanar.IntegerRoots.root620 line 3399
2059. lemma OAI.SharpPlanar.IntegerRoots.root620_contains line 3400
2060. def OAI.SharpPlanar.IntegerRoots.mid621 line 3403
2061. lemma OAI.SharpPlanar.IntegerRoots.mid621_contains line 3404
2062. def OAI.SharpPlanar.IntegerRoots.root621 line 3405
2063. lemma OAI.SharpPlanar.IntegerRoots.root621_contains line 3406
2064. def OAI.SharpPlanar.IntegerRoots.root622 line 3409
2065. lemma OAI.SharpPlanar.IntegerRoots.root622_contains line 3410
2066. def OAI.SharpPlanar.IntegerRoots.mid623 line 3413
2067. lemma OAI.SharpPlanar.IntegerRoots.mid623_contains line 3414
2068. def OAI.SharpPlanar.IntegerRoots.root623 line 3415
2069. lemma OAI.SharpPlanar.IntegerRoots.root623_contains line 3416
2070. def OAI.SharpPlanar.IntegerRoots.root624 line 3419
2071. lemma OAI.SharpPlanar.IntegerRoots.root624_contains line 3420
2072. def OAI.SharpPlanar.IntegerRoots.mid625 line 3423
2073. lemma OAI.SharpPlanar.IntegerRoots.mid625_contains line 3424
2074. def OAI.SharpPlanar.IntegerRoots.root625 line 3425
2075. lemma OAI.SharpPlanar.IntegerRoots.root625_contains line 3426
2076. def OAI.SharpPlanar.IntegerRoots.root626 line 3429
2077. lemma OAI.SharpPlanar.IntegerRoots.root626_contains line 3430
2078. def OAI.SharpPlanar.IntegerRoots.mid627 line 3433
2079. lemma OAI.SharpPlanar.IntegerRoots.mid627_contains line 3434
2080. def OAI.SharpPlanar.IntegerRoots.root627 line 3435
2081. lemma OAI.SharpPlanar.IntegerRoots.root627_contains line 3436
2082. def OAI.SharpPlanar.IntegerRoots.root628 line 3439
2083. lemma OAI.SharpPlanar.IntegerRoots.root628_contains line 3440
2084. def OAI.SharpPlanar.IntegerRoots.mid629 line 3443
2085. lemma OAI.SharpPlanar.IntegerRoots.mid629_contains line 3444
2086. def OAI.SharpPlanar.IntegerRoots.root629 line 3445
2087. lemma OAI.SharpPlanar.IntegerRoots.root629_contains line 3446
2088. def OAI.SharpPlanar.IntegerRoots.root630 line 3449
2089. lemma OAI.SharpPlanar.IntegerRoots.root630_contains line 3450
2090. def OAI.SharpPlanar.IntegerRoots.mid631 line 3453
2091. lemma OAI.SharpPlanar.IntegerRoots.mid631_contains line 3454
2092. def OAI.SharpPlanar.IntegerRoots.root631 line 3455
2093. lemma OAI.SharpPlanar.IntegerRoots.root631_contains line 3456
2094. def OAI.SharpPlanar.IntegerRoots.root632 line 3459
2095. lemma OAI.SharpPlanar.IntegerRoots.root632_contains line 3460
2096. def OAI.SharpPlanar.IntegerRoots.mid633 line 3463
2097. lemma OAI.SharpPlanar.IntegerRoots.mid633_contains line 3464
2098. def OAI.SharpPlanar.IntegerRoots.root633 line 3465
2099. lemma OAI.SharpPlanar.IntegerRoots.root633_contains line 3466
2100. def OAI.SharpPlanar.IntegerRoots.root634 line 3469
2101. lemma OAI.SharpPlanar.IntegerRoots.root634_contains line 3470
2102. def OAI.SharpPlanar.IntegerRoots.mid635 line 3473
2103. lemma OAI.SharpPlanar.IntegerRoots.mid635_contains line 3474
2104. def OAI.SharpPlanar.IntegerRoots.root635 line 3475
2105. lemma OAI.SharpPlanar.IntegerRoots.root635_contains line 3476
2106. def OAI.SharpPlanar.IntegerRoots.root636 line 3479
2107. lemma OAI.SharpPlanar.IntegerRoots.root636_contains line 3480
2108. def OAI.SharpPlanar.IntegerRoots.mid637 line 3483
2109. lemma OAI.SharpPlanar.IntegerRoots.mid637_contains line 3484
2110. def OAI.SharpPlanar.IntegerRoots.root637 line 3485
2111. lemma OAI.SharpPlanar.IntegerRoots.root637_contains line 3486
2112. def OAI.SharpPlanar.IntegerRoots.root638 line 3489
2113. lemma OAI.SharpPlanar.IntegerRoots.root638_contains line 3490
2114. def OAI.SharpPlanar.IntegerRoots.mid639 line 3493
2115. lemma OAI.SharpPlanar.IntegerRoots.mid639_contains line 3494
2116. def OAI.SharpPlanar.IntegerRoots.root639 line 3495
2117. lemma OAI.SharpPlanar.IntegerRoots.root639_contains line 3496
2118. def OAI.SharpPlanar.IntegerRoots.root640 line 3499
2119. lemma OAI.SharpPlanar.IntegerRoots.root640_contains line 3500
2120. def OAI.SharpPlanar.IntegerRoots.mid641 line 3503
2121. lemma OAI.SharpPlanar.IntegerRoots.mid641_contains line 3504
2122. def OAI.SharpPlanar.IntegerRoots.root641 line 3505
2123. lemma OAI.SharpPlanar.IntegerRoots.root641_contains line 3506
2124. def OAI.SharpPlanar.IntegerRoots.root642 line 3509
2125. lemma OAI.SharpPlanar.IntegerRoots.root642_contains line 3510
2126. def OAI.SharpPlanar.IntegerRoots.mid643 line 3513
2127. lemma OAI.SharpPlanar.IntegerRoots.mid643_contains line 3514
2128. def OAI.SharpPlanar.IntegerRoots.root643 line 3515
2129. lemma OAI.SharpPlanar.IntegerRoots.root643_contains line 3516
2130. def OAI.SharpPlanar.IntegerRoots.root644 line 3519
2131. lemma OAI.SharpPlanar.IntegerRoots.root644_contains line 3520
2132. def OAI.SharpPlanar.IntegerRoots.mid645 line 3523
2133. lemma OAI.SharpPlanar.IntegerRoots.mid645_contains line 3524
2134. def OAI.SharpPlanar.IntegerRoots.root645 line 3525
2135. lemma OAI.SharpPlanar.IntegerRoots.root645_contains line 3526
2136. def OAI.SharpPlanar.IntegerRoots.root646 line 3529
2137. lemma OAI.SharpPlanar.IntegerRoots.root646_contains line 3530
2138. def OAI.SharpPlanar.IntegerRoots.mid647 line 3533
2139. lemma OAI.SharpPlanar.IntegerRoots.mid647_contains line 3534
2140. def OAI.SharpPlanar.IntegerRoots.root647 line 3535
2141. lemma OAI.SharpPlanar.IntegerRoots.root647_contains line 3536
2142. def OAI.SharpPlanar.IntegerRoots.root648 line 3539
2143. lemma OAI.SharpPlanar.IntegerRoots.root648_contains line 3540
2144. def OAI.SharpPlanar.IntegerRoots.mid649 line 3543
2145. lemma OAI.SharpPlanar.IntegerRoots.mid649_contains line 3544
2146. def OAI.SharpPlanar.IntegerRoots.root649 line 3545
2147. lemma OAI.SharpPlanar.IntegerRoots.root649_contains line 3546
2148. def OAI.SharpPlanar.IntegerRoots.root650 line 3549
2149. lemma OAI.SharpPlanar.IntegerRoots.root650_contains line 3550
2150. def OAI.SharpPlanar.IntegerRoots.mid651 line 3553
2151. lemma OAI.SharpPlanar.IntegerRoots.mid651_contains line 3554
2152. def OAI.SharpPlanar.IntegerRoots.root651 line 3555
2153. lemma OAI.SharpPlanar.IntegerRoots.root651_contains line 3556
2154. def OAI.SharpPlanar.IntegerRoots.root652 line 3559
2155. lemma OAI.SharpPlanar.IntegerRoots.root652_contains line 3560
2156. def OAI.SharpPlanar.IntegerRoots.mid653 line 3563
2157. lemma OAI.SharpPlanar.IntegerRoots.mid653_contains line 3564
2158. def OAI.SharpPlanar.IntegerRoots.root653 line 3565
2159. lemma OAI.SharpPlanar.IntegerRoots.root653_contains line 3566
2160. def OAI.SharpPlanar.IntegerRoots.root654 line 3569
2161. lemma OAI.SharpPlanar.IntegerRoots.root654_contains line 3570
2162. def OAI.SharpPlanar.IntegerRoots.mid655 line 3573
2163. lemma OAI.SharpPlanar.IntegerRoots.mid655_contains line 3574
2164. def OAI.SharpPlanar.IntegerRoots.root655 line 3575
2165. lemma OAI.SharpPlanar.IntegerRoots.root655_contains line 3576
2166. def OAI.SharpPlanar.IntegerRoots.root656 line 3579
2167. lemma OAI.SharpPlanar.IntegerRoots.root656_contains line 3580
2168. def OAI.SharpPlanar.IntegerRoots.mid657 line 3583
2169. lemma OAI.SharpPlanar.IntegerRoots.mid657_contains line 3584
2170. def OAI.SharpPlanar.IntegerRoots.root657 line 3585
2171. lemma OAI.SharpPlanar.IntegerRoots.root657_contains line 3586
2172. def OAI.SharpPlanar.IntegerRoots.root658 line 3589
2173. lemma OAI.SharpPlanar.IntegerRoots.root658_contains line 3590
2174. def OAI.SharpPlanar.IntegerRoots.mid659 line 3593
2175. lemma OAI.SharpPlanar.IntegerRoots.mid659_contains line 3594
2176. def OAI.SharpPlanar.IntegerRoots.root659 line 3595
2177. lemma OAI.SharpPlanar.IntegerRoots.root659_contains line 3596
2178. def OAI.SharpPlanar.IntegerRoots.root660 line 3599
2179. lemma OAI.SharpPlanar.IntegerRoots.root660_contains line 3600
2180. def OAI.SharpPlanar.IntegerRoots.mid661 line 3603
2181. lemma OAI.SharpPlanar.IntegerRoots.mid661_contains line 3604
2182. def OAI.SharpPlanar.IntegerRoots.root661 line 3605
2183. lemma OAI.SharpPlanar.IntegerRoots.root661_contains line 3606
2184. def OAI.SharpPlanar.IntegerRoots.root662 line 3609
2185. lemma OAI.SharpPlanar.IntegerRoots.root662_contains line 3610
2186. def OAI.SharpPlanar.IntegerRoots.mid663 line 3613
2187. lemma OAI.SharpPlanar.IntegerRoots.mid663_contains line 3614
2188. def OAI.SharpPlanar.IntegerRoots.root663 line 3615
2189. lemma OAI.SharpPlanar.IntegerRoots.root663_contains line 3616
2190. def OAI.SharpPlanar.IntegerRoots.root664 line 3619
2191. lemma OAI.SharpPlanar.IntegerRoots.root664_contains line 3620
2192. def OAI.SharpPlanar.IntegerRoots.mid665 line 3623
2193. lemma OAI.SharpPlanar.IntegerRoots.mid665_contains line 3624
2194. def OAI.SharpPlanar.IntegerRoots.root665 line 3625
2195. lemma OAI.SharpPlanar.IntegerRoots.root665_contains line 3626
2196. def OAI.SharpPlanar.IntegerRoots.root666 line 3629
2197. lemma OAI.SharpPlanar.IntegerRoots.root666_contains line 3630
2198. def OAI.SharpPlanar.IntegerRoots.mid667 line 3633
2199. lemma OAI.SharpPlanar.IntegerRoots.mid667_contains line 3634
2200. def OAI.SharpPlanar.IntegerRoots.root667 line 3635
2201. lemma OAI.SharpPlanar.IntegerRoots.root667_contains line 3636
2202. def OAI.SharpPlanar.IntegerRoots.root668 line 3639
2203. lemma OAI.SharpPlanar.IntegerRoots.root668_contains line 3640
2204. def OAI.SharpPlanar.IntegerRoots.mid669 line 3643
2205. lemma OAI.SharpPlanar.IntegerRoots.mid669_contains line 3644
2206. def OAI.SharpPlanar.IntegerRoots.root669 line 3645
2207. lemma OAI.SharpPlanar.IntegerRoots.root669_contains line 3646
2208. def OAI.SharpPlanar.IntegerRoots.root670 line 3649
2209. lemma OAI.SharpPlanar.IntegerRoots.root670_contains line 3650
2210. def OAI.SharpPlanar.IntegerRoots.mid671 line 3653
2211. lemma OAI.SharpPlanar.IntegerRoots.mid671_contains line 3654
2212. def OAI.SharpPlanar.IntegerRoots.root671 line 3655
2213. lemma OAI.SharpPlanar.IntegerRoots.root671_contains line 3656
2214. def OAI.SharpPlanar.IntegerRoots.root672 line 3659
2215. lemma OAI.SharpPlanar.IntegerRoots.root672_contains line 3660
2216. def OAI.SharpPlanar.IntegerRoots.mid673 line 3663
2217. lemma OAI.SharpPlanar.IntegerRoots.mid673_contains line 3664
2218. def OAI.SharpPlanar.IntegerRoots.root673 line 3665
2219. lemma OAI.SharpPlanar.IntegerRoots.root673_contains line 3666
2220. def OAI.SharpPlanar.IntegerRoots.root674 line 3669
2221. lemma OAI.SharpPlanar.IntegerRoots.root674_contains line 3670
2222. def OAI.SharpPlanar.IntegerRoots.mid675 line 3673
2223. lemma OAI.SharpPlanar.IntegerRoots.mid675_contains line 3674
2224. def OAI.SharpPlanar.IntegerRoots.root675 line 3675
2225. lemma OAI.SharpPlanar.IntegerRoots.root675_contains line 3676
2226. def OAI.SharpPlanar.IntegerRoots.root676 line 3679
2227. lemma OAI.SharpPlanar.IntegerRoots.root676_contains line 3680
2228. def OAI.SharpPlanar.IntegerRoots.mid677 line 3683
2229. lemma OAI.SharpPlanar.IntegerRoots.mid677_contains line 3684
2230. def OAI.SharpPlanar.IntegerRoots.root677 line 3685
2231. lemma OAI.SharpPlanar.IntegerRoots.root677_contains line 3686
2232. def OAI.SharpPlanar.IntegerRoots.root678 line 3689
2233. lemma OAI.SharpPlanar.IntegerRoots.root678_contains line 3690
2234. def OAI.SharpPlanar.IntegerRoots.mid679 line 3693
2235. lemma OAI.SharpPlanar.IntegerRoots.mid679_contains line 3694
2236. def OAI.SharpPlanar.IntegerRoots.root679 line 3695
2237. lemma OAI.SharpPlanar.IntegerRoots.root679_contains line 3696
2238. def OAI.SharpPlanar.IntegerRoots.root680 line 3699
2239. lemma OAI.SharpPlanar.IntegerRoots.root680_contains line 3700
2240. def OAI.SharpPlanar.IntegerRoots.mid681 line 3703
2241. lemma OAI.SharpPlanar.IntegerRoots.mid681_contains line 3704
2242. def OAI.SharpPlanar.IntegerRoots.root681 line 3705
2243. lemma OAI.SharpPlanar.IntegerRoots.root681_contains line 3706
2244. def OAI.SharpPlanar.IntegerRoots.root682 line 3709
2245. lemma OAI.SharpPlanar.IntegerRoots.root682_contains line 3710
2246. def OAI.SharpPlanar.IntegerRoots.mid683 line 3713
2247. lemma OAI.SharpPlanar.IntegerRoots.mid683_contains line 3714
2248. def OAI.SharpPlanar.IntegerRoots.root683 line 3715
2249. lemma OAI.SharpPlanar.IntegerRoots.root683_contains line 3716
2250. def OAI.SharpPlanar.IntegerRoots.root684 line 3719
2251. lemma OAI.SharpPlanar.IntegerRoots.root684_contains line 3720
2252. def OAI.SharpPlanar.IntegerRoots.mid685 line 3723
2253. lemma OAI.SharpPlanar.IntegerRoots.mid685_contains line 3724
2254. def OAI.SharpPlanar.IntegerRoots.root685 line 3725
2255. lemma OAI.SharpPlanar.IntegerRoots.root685_contains line 3726
2256. def OAI.SharpPlanar.IntegerRoots.root686 line 3729
2257. lemma OAI.SharpPlanar.IntegerRoots.root686_contains line 3730
2258. def OAI.SharpPlanar.IntegerRoots.mid687 line 3733
2259. lemma OAI.SharpPlanar.IntegerRoots.mid687_contains line 3734
2260. def OAI.SharpPlanar.IntegerRoots.root687 line 3735
2261. lemma OAI.SharpPlanar.IntegerRoots.root687_contains line 3736
2262. def OAI.SharpPlanar.IntegerRoots.root688 line 3739
2263. lemma OAI.SharpPlanar.IntegerRoots.root688_contains line 3740
2264. def OAI.SharpPlanar.IntegerRoots.mid689 line 3743
2265. lemma OAI.SharpPlanar.IntegerRoots.mid689_contains line 3744
2266. def OAI.SharpPlanar.IntegerRoots.root689 line 3745
2267. lemma OAI.SharpPlanar.IntegerRoots.root689_contains line 3746
2268. def OAI.SharpPlanar.IntegerRoots.root690 line 3749
2269. lemma OAI.SharpPlanar.IntegerRoots.root690_contains line 3750
2270. def OAI.SharpPlanar.IntegerRoots.mid691 line 3753
2271. lemma OAI.SharpPlanar.IntegerRoots.mid691_contains line 3754
2272. def OAI.SharpPlanar.IntegerRoots.root691 line 3755
2273. lemma OAI.SharpPlanar.IntegerRoots.root691_contains line 3756
2274. def OAI.SharpPlanar.IntegerRoots.root692 line 3759
2275. lemma OAI.SharpPlanar.IntegerRoots.root692_contains line 3760
2276. def OAI.SharpPlanar.IntegerRoots.mid693 line 3763
2277. lemma OAI.SharpPlanar.IntegerRoots.mid693_contains line 3764
2278. def OAI.SharpPlanar.IntegerRoots.root693 line 3765
2279. lemma OAI.SharpPlanar.IntegerRoots.root693_contains line 3766
2280. def OAI.SharpPlanar.IntegerRoots.root694 line 3769
2281. lemma OAI.SharpPlanar.IntegerRoots.root694_contains line 3770
2282. def OAI.SharpPlanar.IntegerRoots.mid695 line 3773
2283. lemma OAI.SharpPlanar.IntegerRoots.mid695_contains line 3774
2284. def OAI.SharpPlanar.IntegerRoots.root695 line 3775
2285. lemma OAI.SharpPlanar.IntegerRoots.root695_contains line 3776
2286. def OAI.SharpPlanar.IntegerRoots.root696 line 3779
2287. lemma OAI.SharpPlanar.IntegerRoots.root696_contains line 3780
2288. def OAI.SharpPlanar.IntegerRoots.mid697 line 3783
2289. lemma OAI.SharpPlanar.IntegerRoots.mid697_contains line 3784
2290. def OAI.SharpPlanar.IntegerRoots.root697 line 3785
2291. lemma OAI.SharpPlanar.IntegerRoots.root697_contains line 3786
2292. def OAI.SharpPlanar.IntegerRoots.root698 line 3789
2293. lemma OAI.SharpPlanar.IntegerRoots.root698_contains line 3790
2294. def OAI.SharpPlanar.IntegerRoots.mid699 line 3793
2295. lemma OAI.SharpPlanar.IntegerRoots.mid699_contains line 3794
2296. def OAI.SharpPlanar.IntegerRoots.root699 line 3795
2297. lemma OAI.SharpPlanar.IntegerRoots.root699_contains line 3796
2298. def OAI.SharpPlanar.IntegerRoots.root700 line 3799
2299. lemma OAI.SharpPlanar.IntegerRoots.root700_contains line 3800
2300. def OAI.SharpPlanar.IntegerRoots.mid701 line 3803
2301. lemma OAI.SharpPlanar.IntegerRoots.mid701_contains line 3804
2302. def OAI.SharpPlanar.IntegerRoots.root701 line 3805
2303. lemma OAI.SharpPlanar.IntegerRoots.root701_contains line 3806
2304. def OAI.SharpPlanar.IntegerRoots.root702 line 3809
2305. lemma OAI.SharpPlanar.IntegerRoots.root702_contains line 3810
2306. def OAI.SharpPlanar.IntegerRoots.mid703 line 3813
2307. lemma OAI.SharpPlanar.IntegerRoots.mid703_contains line 3814
2308. def OAI.SharpPlanar.IntegerRoots.root703 line 3815
2309. lemma OAI.SharpPlanar.IntegerRoots.root703_contains line 3816
2310. def OAI.SharpPlanar.IntegerRoots.root704 line 3819
2311. lemma OAI.SharpPlanar.IntegerRoots.root704_contains line 3820
2312. def OAI.SharpPlanar.IntegerRoots.mid705 line 3823
2313. lemma OAI.SharpPlanar.IntegerRoots.mid705_contains line 3824
2314. def OAI.SharpPlanar.IntegerRoots.root705 line 3825
2315. lemma OAI.SharpPlanar.IntegerRoots.root705_contains line 3826
2316. def OAI.SharpPlanar.IntegerRoots.root706 line 3829
2317. lemma OAI.SharpPlanar.IntegerRoots.root706_contains line 3830
2318. def OAI.SharpPlanar.IntegerRoots.mid707 line 3833
2319. lemma OAI.SharpPlanar.IntegerRoots.mid707_contains line 3834
2320. def OAI.SharpPlanar.IntegerRoots.root707 line 3835
2321. lemma OAI.SharpPlanar.IntegerRoots.root707_contains line 3836
2322. def OAI.SharpPlanar.IntegerRoots.root708 line 3839
2323. lemma OAI.SharpPlanar.IntegerRoots.root708_contains line 3840
2324. def OAI.SharpPlanar.IntegerRoots.mid709 line 3843
2325. lemma OAI.SharpPlanar.IntegerRoots.mid709_contains line 3844
2326. def OAI.SharpPlanar.IntegerRoots.root709 line 3845
2327. lemma OAI.SharpPlanar.IntegerRoots.root709_contains line 3846
2328. def OAI.SharpPlanar.IntegerRoots.root710 line 3849
2329. lemma OAI.SharpPlanar.IntegerRoots.root710_contains line 3850
2330. def OAI.SharpPlanar.IntegerRoots.mid711 line 3853
2331. lemma OAI.SharpPlanar.IntegerRoots.mid711_contains line 3854
2332. def OAI.SharpPlanar.IntegerRoots.root711 line 3855
2333. lemma OAI.SharpPlanar.IntegerRoots.root711_contains line 3856
2334. def OAI.SharpPlanar.IntegerRoots.root712 line 3859
2335. lemma OAI.SharpPlanar.IntegerRoots.root712_contains line 3860
2336. def OAI.SharpPlanar.IntegerRoots.mid713 line 3863
2337. lemma OAI.SharpPlanar.IntegerRoots.mid713_contains line 3864
2338. def OAI.SharpPlanar.IntegerRoots.root713 line 3865
2339. lemma OAI.SharpPlanar.IntegerRoots.root713_contains line 3866
2340. def OAI.SharpPlanar.IntegerRoots.root714 line 3869
2341. lemma OAI.SharpPlanar.IntegerRoots.root714_contains line 3870
2342. def OAI.SharpPlanar.IntegerRoots.mid715 line 3873
2343. lemma OAI.SharpPlanar.IntegerRoots.mid715_contains line 3874
2344. def OAI.SharpPlanar.IntegerRoots.root715 line 3875
2345. lemma OAI.SharpPlanar.IntegerRoots.root715_contains line 3876
2346. def OAI.SharpPlanar.IntegerRoots.root716 line 3879
2347. lemma OAI.SharpPlanar.IntegerRoots.root716_contains line 3880
2348. def OAI.SharpPlanar.IntegerRoots.mid717 line 3883
2349. lemma OAI.SharpPlanar.IntegerRoots.mid717_contains line 3884
2350. def OAI.SharpPlanar.IntegerRoots.root717 line 3885
2351. lemma OAI.SharpPlanar.IntegerRoots.root717_contains line 3886
2352. def OAI.SharpPlanar.IntegerRoots.root718 line 3889
2353. lemma OAI.SharpPlanar.IntegerRoots.root718_contains line 3890
2354. def OAI.SharpPlanar.IntegerRoots.mid719 line 3893
2355. lemma OAI.SharpPlanar.IntegerRoots.mid719_contains line 3894
2356. def OAI.SharpPlanar.IntegerRoots.root719 line 3895
2357. lemma OAI.SharpPlanar.IntegerRoots.root719_contains line 3896
2358. def OAI.SharpPlanar.IntegerRoots.root720 line 3899
2359. lemma OAI.SharpPlanar.IntegerRoots.root720_contains line 3900
2360. def OAI.SharpPlanar.IntegerRoots.mid721 line 3903
2361. lemma OAI.SharpPlanar.IntegerRoots.mid721_contains line 3904
2362. def OAI.SharpPlanar.IntegerRoots.root721 line 3905
2363. lemma OAI.SharpPlanar.IntegerRoots.root721_contains line 3906
2364. def OAI.SharpPlanar.IntegerRoots.root722 line 3909
2365. lemma OAI.SharpPlanar.IntegerRoots.root722_contains line 3910
2366. def OAI.SharpPlanar.IntegerRoots.mid723 line 3913
2367. lemma OAI.SharpPlanar.IntegerRoots.mid723_contains line 3914
2368. def OAI.SharpPlanar.IntegerRoots.root723 line 3915
2369. lemma OAI.SharpPlanar.IntegerRoots.root723_contains line 3916
2370. def OAI.SharpPlanar.IntegerRoots.root724 line 3919
2371. lemma OAI.SharpPlanar.IntegerRoots.root724_contains line 3920
2372. def OAI.SharpPlanar.IntegerRoots.mid725 line 3923
2373. lemma OAI.SharpPlanar.IntegerRoots.mid725_contains line 3924
2374. def OAI.SharpPlanar.IntegerRoots.root725 line 3925
2375. lemma OAI.SharpPlanar.IntegerRoots.root725_contains line 3926
2376. def OAI.SharpPlanar.IntegerRoots.root726 line 3929
2377. lemma OAI.SharpPlanar.IntegerRoots.root726_contains line 3930
2378. def OAI.SharpPlanar.IntegerRoots.mid727 line 3933
2379. lemma OAI.SharpPlanar.IntegerRoots.mid727_contains line 3934
2380. def OAI.SharpPlanar.IntegerRoots.root727 line 3935
2381. lemma OAI.SharpPlanar.IntegerRoots.root727_contains line 3936
2382. def OAI.SharpPlanar.IntegerRoots.root728 line 3939
2383. lemma OAI.SharpPlanar.IntegerRoots.root728_contains line 3940
2384. def OAI.SharpPlanar.IntegerRoots.mid729 line 3943
2385. lemma OAI.SharpPlanar.IntegerRoots.mid729_contains line 3944
2386. def OAI.SharpPlanar.IntegerRoots.root729 line 3945
2387. lemma OAI.SharpPlanar.IntegerRoots.root729_contains line 3946
2388. def OAI.SharpPlanar.IntegerRoots.root730 line 3949
2389. lemma OAI.SharpPlanar.IntegerRoots.root730_contains line 3950
2390. def OAI.SharpPlanar.IntegerRoots.mid731 line 3953
2391. lemma OAI.SharpPlanar.IntegerRoots.mid731_contains line 3954
2392. def OAI.SharpPlanar.IntegerRoots.root731 line 3955
2393. lemma OAI.SharpPlanar.IntegerRoots.root731_contains line 3956
2394. def OAI.SharpPlanar.IntegerRoots.root732 line 3959
2395. lemma OAI.SharpPlanar.IntegerRoots.root732_contains line 3960
2396. def OAI.SharpPlanar.IntegerRoots.mid733 line 3963
2397. lemma OAI.SharpPlanar.IntegerRoots.mid733_contains line 3964
2398. def OAI.SharpPlanar.IntegerRoots.root733 line 3965
2399. lemma OAI.SharpPlanar.IntegerRoots.root733_contains line 3966
2400. def OAI.SharpPlanar.IntegerRoots.root734 line 3969
2401. lemma OAI.SharpPlanar.IntegerRoots.root734_contains line 3970
2402. def OAI.SharpPlanar.IntegerRoots.mid735 line 3973
2403. lemma OAI.SharpPlanar.IntegerRoots.mid735_contains line 3974
2404. def OAI.SharpPlanar.IntegerRoots.root735 line 3975
2405. lemma OAI.SharpPlanar.IntegerRoots.root735_contains line 3976
2406. def OAI.SharpPlanar.IntegerRoots.root736 line 3979
2407. lemma OAI.SharpPlanar.IntegerRoots.root736_contains line 3980
2408. def OAI.SharpPlanar.IntegerRoots.mid737 line 3983
2409. lemma OAI.SharpPlanar.IntegerRoots.mid737_contains line 3984
2410. def OAI.SharpPlanar.IntegerRoots.root737 line 3985
2411. lemma OAI.SharpPlanar.IntegerRoots.root737_contains line 3986
2412. def OAI.SharpPlanar.IntegerRoots.root738 line 3989
2413. lemma OAI.SharpPlanar.IntegerRoots.root738_contains line 3990
2414. def OAI.SharpPlanar.IntegerRoots.mid739 line 3993
2415. lemma OAI.SharpPlanar.IntegerRoots.mid739_contains line 3994
2416. def OAI.SharpPlanar.IntegerRoots.root739 line 3995
2417. lemma OAI.SharpPlanar.IntegerRoots.root739_contains line 3996
2418. def OAI.SharpPlanar.IntegerRoots.root740 line 3999
2419. lemma OAI.SharpPlanar.IntegerRoots.root740_contains line 4000
2420. def OAI.SharpPlanar.IntegerRoots.mid741 line 4003
2421. lemma OAI.SharpPlanar.IntegerRoots.mid741_contains line 4004
2422. def OAI.SharpPlanar.IntegerRoots.root741 line 4005
2423. lemma OAI.SharpPlanar.IntegerRoots.root741_contains line 4006
2424. def OAI.SharpPlanar.IntegerRoots.root742 line 4009
2425. lemma OAI.SharpPlanar.IntegerRoots.root742_contains line 4010
2426. def OAI.SharpPlanar.IntegerRoots.mid743 line 4013
2427. lemma OAI.SharpPlanar.IntegerRoots.mid743_contains line 4014
2428. def OAI.SharpPlanar.IntegerRoots.root743 line 4015
2429. lemma OAI.SharpPlanar.IntegerRoots.root743_contains line 4016
2430. def OAI.SharpPlanar.IntegerRoots.root744 line 4019
2431. lemma OAI.SharpPlanar.IntegerRoots.root744_contains line 4020
2432. def OAI.SharpPlanar.IntegerRoots.mid745 line 4023
2433. lemma OAI.SharpPlanar.IntegerRoots.mid745_contains line 4024
2434. def OAI.SharpPlanar.IntegerRoots.root745 line 4025
2435. lemma OAI.SharpPlanar.IntegerRoots.root745_contains line 4026
2436. def OAI.SharpPlanar.IntegerRoots.root746 line 4029
2437. lemma OAI.SharpPlanar.IntegerRoots.root746_contains line 4030
2438. def OAI.SharpPlanar.IntegerRoots.mid747 line 4033
2439. lemma OAI.SharpPlanar.IntegerRoots.mid747_contains line 4034
2440. def OAI.SharpPlanar.IntegerRoots.root747 line 4035
2441. lemma OAI.SharpPlanar.IntegerRoots.root747_contains line 4036
2442. def OAI.SharpPlanar.IntegerRoots.root748 line 4039
2443. lemma OAI.SharpPlanar.IntegerRoots.root748_contains line 4040
2444. def OAI.SharpPlanar.IntegerRoots.mid749 line 4043
2445. lemma OAI.SharpPlanar.IntegerRoots.mid749_contains line 4044
2446. def OAI.SharpPlanar.IntegerRoots.root749 line 4045
2447. lemma OAI.SharpPlanar.IntegerRoots.root749_contains line 4046
2448. def OAI.SharpPlanar.IntegerRoots.root750 line 4049
2449. lemma OAI.SharpPlanar.IntegerRoots.root750_contains line 4050
2450. def OAI.SharpPlanar.IntegerRoots.mid751 line 4053
2451. lemma OAI.SharpPlanar.IntegerRoots.mid751_contains line 4054
2452. def OAI.SharpPlanar.IntegerRoots.root751 line 4055
2453. lemma OAI.SharpPlanar.IntegerRoots.root751_contains line 4056
2454. def OAI.SharpPlanar.IntegerRoots.root752 line 4059
2455. lemma OAI.SharpPlanar.IntegerRoots.root752_contains line 4060
2456. def OAI.SharpPlanar.IntegerRoots.mid753 line 4063
2457. lemma OAI.SharpPlanar.IntegerRoots.mid753_contains line 4064
2458. def OAI.SharpPlanar.IntegerRoots.root753 line 4065
2459. lemma OAI.SharpPlanar.IntegerRoots.root753_contains line 4066
2460. def OAI.SharpPlanar.IntegerRoots.root754 line 4069
2461. lemma OAI.SharpPlanar.IntegerRoots.root754_contains line 4070
2462. def OAI.SharpPlanar.IntegerRoots.mid755 line 4073
2463. lemma OAI.SharpPlanar.IntegerRoots.mid755_contains line 4074
2464. def OAI.SharpPlanar.IntegerRoots.root755 line 4075
2465. lemma OAI.SharpPlanar.IntegerRoots.root755_contains line 4076
2466. def OAI.SharpPlanar.IntegerRoots.root756 line 4079
2467. lemma OAI.SharpPlanar.IntegerRoots.root756_contains line 4080
2468. def OAI.SharpPlanar.IntegerRoots.mid757 line 4083
2469. lemma OAI.SharpPlanar.IntegerRoots.mid757_contains line 4084
2470. def OAI.SharpPlanar.IntegerRoots.root757 line 4085
2471. lemma OAI.SharpPlanar.IntegerRoots.root757_contains line 4086
2472. def OAI.SharpPlanar.IntegerRoots.root758 line 4089
2473. lemma OAI.SharpPlanar.IntegerRoots.root758_contains line 4090
2474. def OAI.SharpPlanar.IntegerRoots.mid759 line 4093
2475. lemma OAI.SharpPlanar.IntegerRoots.mid759_contains line 4094
2476. def OAI.SharpPlanar.IntegerRoots.root759 line 4095
2477. lemma OAI.SharpPlanar.IntegerRoots.root759_contains line 4096
2478. def OAI.SharpPlanar.IntegerRoots.root760 line 4099
2479. lemma OAI.SharpPlanar.IntegerRoots.root760_contains line 4100
2480. def OAI.SharpPlanar.IntegerRoots.mid761 line 4103
2481. lemma OAI.SharpPlanar.IntegerRoots.mid761_contains line 4104
2482. def OAI.SharpPlanar.IntegerRoots.root761 line 4105
2483. lemma OAI.SharpPlanar.IntegerRoots.root761_contains line 4106
2484. def OAI.SharpPlanar.IntegerRoots.root762 line 4109
2485. lemma OAI.SharpPlanar.IntegerRoots.root762_contains line 4110
2486. def OAI.SharpPlanar.IntegerRoots.mid763 line 4113
2487. lemma OAI.SharpPlanar.IntegerRoots.mid763_contains line 4114
2488. def OAI.SharpPlanar.IntegerRoots.root763 line 4115
2489. lemma OAI.SharpPlanar.IntegerRoots.root763_contains line 4116
2490. def OAI.SharpPlanar.IntegerRoots.root764 line 4119
2491. lemma OAI.SharpPlanar.IntegerRoots.root764_contains line 4120
2492. def OAI.SharpPlanar.IntegerRoots.mid765 line 4123
2493. lemma OAI.SharpPlanar.IntegerRoots.mid765_contains line 4124
2494. def OAI.SharpPlanar.IntegerRoots.root765 line 4125
2495. lemma OAI.SharpPlanar.IntegerRoots.root765_contains line 4126
2496. def OAI.SharpPlanar.IntegerRoots.root766 line 4129
2497. lemma OAI.SharpPlanar.IntegerRoots.root766_contains line 4130
2498. def OAI.SharpPlanar.IntegerRoots.mid767 line 4133
2499. lemma OAI.SharpPlanar.IntegerRoots.mid767_contains line 4134
2500. def OAI.SharpPlanar.IntegerRoots.root767 line 4135
2501. lemma OAI.SharpPlanar.IntegerRoots.root767_contains line 4136
2502. def OAI.SharpPlanar.IntegerRoots.root768 line 4139
2503. lemma OAI.SharpPlanar.IntegerRoots.root768_contains line 4140
2504. def OAI.SharpPlanar.IntegerRoots.mid769 line 4143
2505. lemma OAI.SharpPlanar.IntegerRoots.mid769_contains line 4144
2506. def OAI.SharpPlanar.IntegerRoots.root769 line 4145
2507. lemma OAI.SharpPlanar.IntegerRoots.root769_contains line 4146
2508. def OAI.SharpPlanar.IntegerRoots.root770 line 4149
2509. lemma OAI.SharpPlanar.IntegerRoots.root770_contains line 4150
2510. def OAI.SharpPlanar.IntegerRoots.mid771 line 4153
2511. lemma OAI.SharpPlanar.IntegerRoots.mid771_contains line 4154
2512. def OAI.SharpPlanar.IntegerRoots.root771 line 4155
2513. lemma OAI.SharpPlanar.IntegerRoots.root771_contains line 4156
2514. def OAI.SharpPlanar.IntegerRoots.root772 line 4159
2515. lemma OAI.SharpPlanar.IntegerRoots.root772_contains line 4160
2516. def OAI.SharpPlanar.IntegerRoots.mid773 line 4163
2517. lemma OAI.SharpPlanar.IntegerRoots.mid773_contains line 4164
2518. def OAI.SharpPlanar.IntegerRoots.root773 line 4165
2519. lemma OAI.SharpPlanar.IntegerRoots.root773_contains line 4166
2520. def OAI.SharpPlanar.IntegerRoots.root774 line 4169
2521. lemma OAI.SharpPlanar.IntegerRoots.root774_contains line 4170
2522. def OAI.SharpPlanar.IntegerRoots.mid775 line 4173
2523. lemma OAI.SharpPlanar.IntegerRoots.mid775_contains line 4174
2524. def OAI.SharpPlanar.IntegerRoots.root775 line 4175
2525. lemma OAI.SharpPlanar.IntegerRoots.root775_contains line 4176
2526. def OAI.SharpPlanar.IntegerRoots.root776 line 4179
2527. lemma OAI.SharpPlanar.IntegerRoots.root776_contains line 4180
2528. def OAI.SharpPlanar.IntegerRoots.mid777 line 4183
2529. lemma OAI.SharpPlanar.IntegerRoots.mid777_contains line 4184
2530. def OAI.SharpPlanar.IntegerRoots.root777 line 4185
2531. lemma OAI.SharpPlanar.IntegerRoots.root777_contains line 4186
2532. def OAI.SharpPlanar.IntegerRoots.root778 line 4189
2533. lemma OAI.SharpPlanar.IntegerRoots.root778_contains line 4190
2534. def OAI.SharpPlanar.IntegerRoots.mid779 line 4193
2535. lemma OAI.SharpPlanar.IntegerRoots.mid779_contains line 4194
2536. def OAI.SharpPlanar.IntegerRoots.root779 line 4195
2537. lemma OAI.SharpPlanar.IntegerRoots.root779_contains line 4196
2538. def OAI.SharpPlanar.IntegerRoots.root780 line 4199
2539. lemma OAI.SharpPlanar.IntegerRoots.root780_contains line 4200
2540. def OAI.SharpPlanar.IntegerRoots.mid781 line 4203
2541. lemma OAI.SharpPlanar.IntegerRoots.mid781_contains line 4204
2542. def OAI.SharpPlanar.IntegerRoots.root781 line 4205
2543. lemma OAI.SharpPlanar.IntegerRoots.root781_contains line 4206
2544. def OAI.SharpPlanar.IntegerRoots.root782 line 4209
2545. lemma OAI.SharpPlanar.IntegerRoots.root782_contains line 4210
2546. def OAI.SharpPlanar.IntegerRoots.mid783 line 4213
2547. lemma OAI.SharpPlanar.IntegerRoots.mid783_contains line 4214
2548. def OAI.SharpPlanar.IntegerRoots.root783 line 4215
2549. lemma OAI.SharpPlanar.IntegerRoots.root783_contains line 4216
2550. def OAI.SharpPlanar.IntegerRoots.root784 line 4219
2551. lemma OAI.SharpPlanar.IntegerRoots.root784_contains line 4220
2552. def OAI.SharpPlanar.IntegerRoots.mid785 line 4223
2553. lemma OAI.SharpPlanar.IntegerRoots.mid785_contains line 4224
2554. def OAI.SharpPlanar.IntegerRoots.root785 line 4225
2555. lemma OAI.SharpPlanar.IntegerRoots.root785_contains line 4226
2556. def OAI.SharpPlanar.IntegerRoots.root786 line 4229
2557. lemma OAI.SharpPlanar.IntegerRoots.root786_contains line 4230
2558. def OAI.SharpPlanar.IntegerRoots.mid787 line 4233
2559. lemma OAI.SharpPlanar.IntegerRoots.mid787_contains line 4234
2560. def OAI.SharpPlanar.IntegerRoots.root787 line 4235
2561. lemma OAI.SharpPlanar.IntegerRoots.root787_contains line 4236
2562. def OAI.SharpPlanar.IntegerRoots.root788 line 4239
2563. lemma OAI.SharpPlanar.IntegerRoots.root788_contains line 4240
2564. def OAI.SharpPlanar.IntegerRoots.mid789 line 4243
2565. lemma OAI.SharpPlanar.IntegerRoots.mid789_contains line 4244
2566. def OAI.SharpPlanar.IntegerRoots.root789 line 4245
2567. lemma OAI.SharpPlanar.IntegerRoots.root789_contains line 4246
2568. def OAI.SharpPlanar.IntegerRoots.root790 line 4249
2569. lemma OAI.SharpPlanar.IntegerRoots.root790_contains line 4250
2570. def OAI.SharpPlanar.IntegerRoots.mid791 line 4253
2571. lemma OAI.SharpPlanar.IntegerRoots.mid791_contains line 4254
2572. def OAI.SharpPlanar.IntegerRoots.root791 line 4255
2573. lemma OAI.SharpPlanar.IntegerRoots.root791_contains line 4256
2574. def OAI.SharpPlanar.IntegerRoots.root792 line 4259
2575. lemma OAI.SharpPlanar.IntegerRoots.root792_contains line 4260
2576. def OAI.SharpPlanar.IntegerRoots.mid793 line 4263
2577. lemma OAI.SharpPlanar.IntegerRoots.mid793_contains line 4264
2578. def OAI.SharpPlanar.IntegerRoots.root793 line 4265
2579. lemma OAI.SharpPlanar.IntegerRoots.root793_contains line 4266
2580. def OAI.SharpPlanar.IntegerRoots.root794 line 4269
2581. lemma OAI.SharpPlanar.IntegerRoots.root794_contains line 4270
2582. def OAI.SharpPlanar.IntegerRoots.mid795 line 4273
2583. lemma OAI.SharpPlanar.IntegerRoots.mid795_contains line 4274
2584. def OAI.SharpPlanar.IntegerRoots.root795 line 4275
2585. lemma OAI.SharpPlanar.IntegerRoots.root795_contains line 4276
2586. def OAI.SharpPlanar.IntegerRoots.root796 line 4279
2587. lemma OAI.SharpPlanar.IntegerRoots.root796_contains line 4280
2588. def OAI.SharpPlanar.IntegerRoots.mid797 line 4283
2589. lemma OAI.SharpPlanar.IntegerRoots.mid797_contains line 4284
2590. def OAI.SharpPlanar.IntegerRoots.root797 line 4285
2591. lemma OAI.SharpPlanar.IntegerRoots.root797_contains line 4286
2592. def OAI.SharpPlanar.IntegerRoots.root798 line 4289
2593. lemma OAI.SharpPlanar.IntegerRoots.root798_contains line 4290
2594. def OAI.SharpPlanar.IntegerRoots.mid799 line 4293
2595. lemma OAI.SharpPlanar.IntegerRoots.mid799_contains line 4294
2596. def OAI.SharpPlanar.IntegerRoots.root799 line 4295
2597. lemma OAI.SharpPlanar.IntegerRoots.root799_contains line 4296
2598. def OAI.SharpPlanar.IntegerRoots.root800 line 4299
2599. lemma OAI.SharpPlanar.IntegerRoots.root800_contains line 4300
2600. def OAI.SharpPlanar.IntegerRoots.mid801 line 4303
2601. lemma OAI.SharpPlanar.IntegerRoots.mid801_contains line 4304
2602. def OAI.SharpPlanar.IntegerRoots.root801 line 4305
2603. lemma OAI.SharpPlanar.IntegerRoots.root801_contains line 4306
2604. def OAI.SharpPlanar.IntegerRoots.root802 line 4309
2605. lemma OAI.SharpPlanar.IntegerRoots.root802_contains line 4310
2606. def OAI.SharpPlanar.IntegerRoots.mid803 line 4313
2607. lemma OAI.SharpPlanar.IntegerRoots.mid803_contains line 4314
2608. def OAI.SharpPlanar.IntegerRoots.root803 line 4315
2609. lemma OAI.SharpPlanar.IntegerRoots.root803_contains line 4316
2610. def OAI.SharpPlanar.IntegerRoots.root804 line 4319
2611. lemma OAI.SharpPlanar.IntegerRoots.root804_contains line 4320
2612. def OAI.SharpPlanar.IntegerRoots.mid805 line 4323
2613. lemma OAI.SharpPlanar.IntegerRoots.mid805_contains line 4324
2614. def OAI.SharpPlanar.IntegerRoots.root805 line 4325
2615. lemma OAI.SharpPlanar.IntegerRoots.root805_contains line 4326
2616. def OAI.SharpPlanar.IntegerRoots.root806 line 4329
2617. lemma OAI.SharpPlanar.IntegerRoots.root806_contains line 4330
2618. def OAI.SharpPlanar.IntegerRoots.mid807 line 4333
2619. lemma OAI.SharpPlanar.IntegerRoots.mid807_contains line 4334
2620. def OAI.SharpPlanar.IntegerRoots.root807 line 4335
2621. lemma OAI.SharpPlanar.IntegerRoots.root807_contains line 4336
2622. def OAI.SharpPlanar.IntegerRoots.root808 line 4339
2623. lemma OAI.SharpPlanar.IntegerRoots.root808_contains line 4340
2624. def OAI.SharpPlanar.IntegerRoots.mid809 line 4343
2625. lemma OAI.SharpPlanar.IntegerRoots.mid809_contains line 4344
2626. def OAI.SharpPlanar.IntegerRoots.root809 line 4345
2627. lemma OAI.SharpPlanar.IntegerRoots.root809_contains line 4346
2628. def OAI.SharpPlanar.IntegerRoots.root810 line 4349
2629. lemma OAI.SharpPlanar.IntegerRoots.root810_contains line 4350
2630. def OAI.SharpPlanar.IntegerRoots.mid811 line 4353
2631. lemma OAI.SharpPlanar.IntegerRoots.mid811_contains line 4354
2632. def OAI.SharpPlanar.IntegerRoots.root811 line 4355
2633. lemma OAI.SharpPlanar.IntegerRoots.root811_contains line 4356
2634. def OAI.SharpPlanar.IntegerRoots.root812 line 4359
2635. lemma OAI.SharpPlanar.IntegerRoots.root812_contains line 4360
2636. def OAI.SharpPlanar.IntegerRoots.mid813 line 4363
2637. lemma OAI.SharpPlanar.IntegerRoots.mid813_contains line 4364
2638. def OAI.SharpPlanar.IntegerRoots.root813 line 4365
2639. lemma OAI.SharpPlanar.IntegerRoots.root813_contains line 4366
2640. def OAI.SharpPlanar.IntegerRoots.root814 line 4369
2641. lemma OAI.SharpPlanar.IntegerRoots.root814_contains line 4370
2642. def OAI.SharpPlanar.IntegerRoots.mid815 line 4373
2643. lemma OAI.SharpPlanar.IntegerRoots.mid815_contains line 4374
2644. def OAI.SharpPlanar.IntegerRoots.root815 line 4375
2645. lemma OAI.SharpPlanar.IntegerRoots.root815_contains line 4376
2646. def OAI.SharpPlanar.IntegerRoots.root816 line 4379
2647. lemma OAI.SharpPlanar.IntegerRoots.root816_contains line 4380
2648. def OAI.SharpPlanar.IntegerRoots.mid817 line 4383
2649. lemma OAI.SharpPlanar.IntegerRoots.mid817_contains line 4384
2650. def OAI.SharpPlanar.IntegerRoots.root817 line 4385
2651. lemma OAI.SharpPlanar.IntegerRoots.root817_contains line 4386
2652. def OAI.SharpPlanar.IntegerRoots.root818 line 4389
2653. lemma OAI.SharpPlanar.IntegerRoots.root818_contains line 4390
2654. def OAI.SharpPlanar.IntegerRoots.mid819 line 4393
2655. lemma OAI.SharpPlanar.IntegerRoots.mid819_contains line 4394
2656. def OAI.SharpPlanar.IntegerRoots.root819 line 4395
2657. lemma OAI.SharpPlanar.IntegerRoots.root819_contains line 4396
2658. def OAI.SharpPlanar.IntegerRoots.root820 line 4399
2659. lemma OAI.SharpPlanar.IntegerRoots.root820_contains line 4400
2660. def OAI.SharpPlanar.IntegerRoots.mid821 line 4403
2661. lemma OAI.SharpPlanar.IntegerRoots.mid821_contains line 4404
2662. def OAI.SharpPlanar.IntegerRoots.root821 line 4405
2663. lemma OAI.SharpPlanar.IntegerRoots.root821_contains line 4406
2664. def OAI.SharpPlanar.IntegerRoots.root822 line 4409
2665. lemma OAI.SharpPlanar.IntegerRoots.root822_contains line 4410
2666. def OAI.SharpPlanar.IntegerRoots.mid823 line 4413
2667. lemma OAI.SharpPlanar.IntegerRoots.mid823_contains line 4414
2668. def OAI.SharpPlanar.IntegerRoots.root823 line 4415
2669. lemma OAI.SharpPlanar.IntegerRoots.root823_contains line 4416
2670. def OAI.SharpPlanar.IntegerRoots.root824 line 4419
2671. lemma OAI.SharpPlanar.IntegerRoots.root824_contains line 4420
2672. def OAI.SharpPlanar.IntegerRoots.mid825 line 4423
2673. lemma OAI.SharpPlanar.IntegerRoots.mid825_contains line 4424
2674. def OAI.SharpPlanar.IntegerRoots.root825 line 4425
2675. lemma OAI.SharpPlanar.IntegerRoots.root825_contains line 4426
2676. def OAI.SharpPlanar.IntegerRoots.root826 line 4429
2677. lemma OAI.SharpPlanar.IntegerRoots.root826_contains line 4430
2678. def OAI.SharpPlanar.IntegerRoots.mid827 line 4433
2679. lemma OAI.SharpPlanar.IntegerRoots.mid827_contains line 4434
2680. def OAI.SharpPlanar.IntegerRoots.root827 line 4435
2681. lemma OAI.SharpPlanar.IntegerRoots.root827_contains line 4436
2682. def OAI.SharpPlanar.IntegerRoots.root828 line 4439
2683. lemma OAI.SharpPlanar.IntegerRoots.root828_contains line 4440
2684. def OAI.SharpPlanar.IntegerRoots.mid829 line 4443
2685. lemma OAI.SharpPlanar.IntegerRoots.mid829_contains line 4444
2686. def OAI.SharpPlanar.IntegerRoots.root829 line 4445
2687. lemma OAI.SharpPlanar.IntegerRoots.root829_contains line 4446
2688. def OAI.SharpPlanar.IntegerRoots.root830 line 4449
2689. lemma OAI.SharpPlanar.IntegerRoots.root830_contains line 4450
2690. def OAI.SharpPlanar.IntegerRoots.mid831 line 4453
2691. lemma OAI.SharpPlanar.IntegerRoots.mid831_contains line 4454
2692. def OAI.SharpPlanar.IntegerRoots.root831 line 4455
2693. lemma OAI.SharpPlanar.IntegerRoots.root831_contains line 4456
2694. def OAI.SharpPlanar.IntegerRoots.root832 line 4459
2695. lemma OAI.SharpPlanar.IntegerRoots.root832_contains line 4460
2696. def OAI.SharpPlanar.IntegerRoots.mid833 line 4463
2697. lemma OAI.SharpPlanar.IntegerRoots.mid833_contains line 4464
2698. def OAI.SharpPlanar.IntegerRoots.root833 line 4465
2699. lemma OAI.SharpPlanar.IntegerRoots.root833_contains line 4466
2700. def OAI.SharpPlanar.IntegerRoots.root834 line 4469
2701. lemma OAI.SharpPlanar.IntegerRoots.root834_contains line 4470
2702. def OAI.SharpPlanar.IntegerRoots.mid835 line 4473
2703. lemma OAI.SharpPlanar.IntegerRoots.mid835_contains line 4474
2704. def OAI.SharpPlanar.IntegerRoots.root835 line 4475
2705. lemma OAI.SharpPlanar.IntegerRoots.root835_contains line 4476
2706. def OAI.SharpPlanar.IntegerRoots.root836 line 4479
2707. lemma OAI.SharpPlanar.IntegerRoots.root836_contains line 4480
2708. def OAI.SharpPlanar.IntegerRoots.mid837 line 4483
2709. lemma OAI.SharpPlanar.IntegerRoots.mid837_contains line 4484
2710. def OAI.SharpPlanar.IntegerRoots.root837 line 4485
2711. lemma OAI.SharpPlanar.IntegerRoots.root837_contains line 4486
2712. def OAI.SharpPlanar.IntegerRoots.root838 line 4489
2713. lemma OAI.SharpPlanar.IntegerRoots.root838_contains line 4490
2714. def OAI.SharpPlanar.IntegerRoots.mid839 line 4493
2715. lemma OAI.SharpPlanar.IntegerRoots.mid839_contains line 4494
2716. def OAI.SharpPlanar.IntegerRoots.root839 line 4495
2717. lemma OAI.SharpPlanar.IntegerRoots.root839_contains line 4496
2718. def OAI.SharpPlanar.IntegerRoots.root840 line 4499
2719. lemma OAI.SharpPlanar.IntegerRoots.root840_contains line 4500
2720. def OAI.SharpPlanar.IntegerRoots.mid841 line 4503
2721. lemma OAI.SharpPlanar.IntegerRoots.mid841_contains line 4504
2722. def OAI.SharpPlanar.IntegerRoots.root841 line 4505
2723. lemma OAI.SharpPlanar.IntegerRoots.root841_contains line 4506
2724. def OAI.SharpPlanar.IntegerRoots.root842 line 4509
2725. lemma OAI.SharpPlanar.IntegerRoots.root842_contains line 4510
2726. def OAI.SharpPlanar.IntegerRoots.mid843 line 4513
2727. lemma OAI.SharpPlanar.IntegerRoots.mid843_contains line 4514
2728. def OAI.SharpPlanar.IntegerRoots.root843 line 4515
2729. lemma OAI.SharpPlanar.IntegerRoots.root843_contains line 4516
2730. def OAI.SharpPlanar.IntegerRoots.root844 line 4519
2731. lemma OAI.SharpPlanar.IntegerRoots.root844_contains line 4520
2732. def OAI.SharpPlanar.IntegerRoots.mid845 line 4523
2733. lemma OAI.SharpPlanar.IntegerRoots.mid845_contains line 4524
2734. def OAI.SharpPlanar.IntegerRoots.root845 line 4525
2735. lemma OAI.SharpPlanar.IntegerRoots.root845_contains line 4526
2736. def OAI.SharpPlanar.IntegerRoots.root846 line 4529
2737. lemma OAI.SharpPlanar.IntegerRoots.root846_contains line 4530
2738. def OAI.SharpPlanar.IntegerRoots.mid847 line 4533
2739. lemma OAI.SharpPlanar.IntegerRoots.mid847_contains line 4534
2740. def OAI.SharpPlanar.IntegerRoots.root847 line 4535
2741. lemma OAI.SharpPlanar.IntegerRoots.root847_contains line 4536
2742. def OAI.SharpPlanar.IntegerRoots.root848 line 4539
2743. lemma OAI.SharpPlanar.IntegerRoots.root848_contains line 4540
2744. def OAI.SharpPlanar.IntegerRoots.mid849 line 4543
2745. lemma OAI.SharpPlanar.IntegerRoots.mid849_contains line 4544
2746. def OAI.SharpPlanar.IntegerRoots.root849 line 4545
2747. lemma OAI.SharpPlanar.IntegerRoots.root849_contains line 4546
2748. def OAI.SharpPlanar.IntegerRoots.root850 line 4549
2749. lemma OAI.SharpPlanar.IntegerRoots.root850_contains line 4550
2750. def OAI.SharpPlanar.IntegerRoots.mid851 line 4553
2751. lemma OAI.SharpPlanar.IntegerRoots.mid851_contains line 4554
2752. def OAI.SharpPlanar.IntegerRoots.root851 line 4555
2753. lemma OAI.SharpPlanar.IntegerRoots.root851_contains line 4556
2754. def OAI.SharpPlanar.IntegerRoots.root852 line 4559
2755. lemma OAI.SharpPlanar.IntegerRoots.root852_contains line 4560
2756. def OAI.SharpPlanar.IntegerRoots.mid853 line 4563
2757. lemma OAI.SharpPlanar.IntegerRoots.mid853_contains line 4564
2758. def OAI.SharpPlanar.IntegerRoots.root853 line 4565
2759. lemma OAI.SharpPlanar.IntegerRoots.root853_contains line 4566
2760. def OAI.SharpPlanar.IntegerRoots.root854 line 4569
2761. lemma OAI.SharpPlanar.IntegerRoots.root854_contains line 4570
2762. def OAI.SharpPlanar.IntegerRoots.mid855 line 4573
2763. lemma OAI.SharpPlanar.IntegerRoots.mid855_contains line 4574
2764. def OAI.SharpPlanar.IntegerRoots.root855 line 4575
2765. lemma OAI.SharpPlanar.IntegerRoots.root855_contains line 4576
2766. def OAI.SharpPlanar.IntegerRoots.root856 line 4579
2767. lemma OAI.SharpPlanar.IntegerRoots.root856_contains line 4580
2768. def OAI.SharpPlanar.IntegerRoots.mid857 line 4583
2769. lemma OAI.SharpPlanar.IntegerRoots.mid857_contains line 4584
2770. def OAI.SharpPlanar.IntegerRoots.root857 line 4585
2771. lemma OAI.SharpPlanar.IntegerRoots.root857_contains line 4586
2772. def OAI.SharpPlanar.IntegerRoots.root858 line 4589
2773. lemma OAI.SharpPlanar.IntegerRoots.root858_contains line 4590
2774. def OAI.SharpPlanar.IntegerRoots.mid859 line 4593
2775. lemma OAI.SharpPlanar.IntegerRoots.mid859_contains line 4594
2776. def OAI.SharpPlanar.IntegerRoots.root859 line 4595
2777. lemma OAI.SharpPlanar.IntegerRoots.root859_contains line 4596
2778. def OAI.SharpPlanar.IntegerRoots.root860 line 4599
2779. lemma OAI.SharpPlanar.IntegerRoots.root860_contains line 4600
2780. def OAI.SharpPlanar.IntegerRoots.mid861 line 4603
2781. lemma OAI.SharpPlanar.IntegerRoots.mid861_contains line 4604
2782. def OAI.SharpPlanar.IntegerRoots.root861 line 4605
2783. lemma OAI.SharpPlanar.IntegerRoots.root861_contains line 4606
2784. def OAI.SharpPlanar.IntegerRoots.root862 line 4609
2785. lemma OAI.SharpPlanar.IntegerRoots.root862_contains line 4610
2786. def OAI.SharpPlanar.IntegerRoots.mid863 line 4613
2787. lemma OAI.SharpPlanar.IntegerRoots.mid863_contains line 4614
2788. def OAI.SharpPlanar.IntegerRoots.root863 line 4615
2789. lemma OAI.SharpPlanar.IntegerRoots.root863_contains line 4616
2790. def OAI.SharpPlanar.IntegerRoots.root864 line 4619
2791. lemma OAI.SharpPlanar.IntegerRoots.root864_contains line 4620
2792. def OAI.SharpPlanar.IntegerRoots.mid865 line 4623
2793. lemma OAI.SharpPlanar.IntegerRoots.mid865_contains line 4624
2794. def OAI.SharpPlanar.IntegerRoots.root865 line 4625
2795. lemma OAI.SharpPlanar.IntegerRoots.root865_contains line 4626
2796. def OAI.SharpPlanar.IntegerRoots.root866 line 4629
2797. lemma OAI.SharpPlanar.IntegerRoots.root866_contains line 4630
2798. def OAI.SharpPlanar.IntegerRoots.mid867 line 4633
2799. lemma OAI.SharpPlanar.IntegerRoots.mid867_contains line 4634
2800. def OAI.SharpPlanar.IntegerRoots.root867 line 4635
2801. lemma OAI.SharpPlanar.IntegerRoots.root867_contains line 4636
2802. def OAI.SharpPlanar.IntegerRoots.root868 line 4639
2803. lemma OAI.SharpPlanar.IntegerRoots.root868_contains line 4640
2804. def OAI.SharpPlanar.IntegerRoots.mid869 line 4643
2805. lemma OAI.SharpPlanar.IntegerRoots.mid869_contains line 4644
2806. def OAI.SharpPlanar.IntegerRoots.root869 line 4645
2807. lemma OAI.SharpPlanar.IntegerRoots.root869_contains line 4646
2808. def OAI.SharpPlanar.IntegerRoots.root870 line 4649
2809. lemma OAI.SharpPlanar.IntegerRoots.root870_contains line 4650
2810. def OAI.SharpPlanar.IntegerRoots.mid871 line 4653
2811. lemma OAI.SharpPlanar.IntegerRoots.mid871_contains line 4654
2812. def OAI.SharpPlanar.IntegerRoots.root871 line 4655
2813. lemma OAI.SharpPlanar.IntegerRoots.root871_contains line 4656
2814. def OAI.SharpPlanar.IntegerRoots.root872 line 4659
2815. lemma OAI.SharpPlanar.IntegerRoots.root872_contains line 4660
2816. def OAI.SharpPlanar.IntegerRoots.mid873 line 4663
2817. lemma OAI.SharpPlanar.IntegerRoots.mid873_contains line 4664
2818. def OAI.SharpPlanar.IntegerRoots.root873 line 4665
2819. lemma OAI.SharpPlanar.IntegerRoots.root873_contains line 4666
2820. def OAI.SharpPlanar.IntegerRoots.root874 line 4669
2821. lemma OAI.SharpPlanar.IntegerRoots.root874_contains line 4670
2822. def OAI.SharpPlanar.IntegerRoots.mid875 line 4673
2823. lemma OAI.SharpPlanar.IntegerRoots.mid875_contains line 4674
2824. def OAI.SharpPlanar.IntegerRoots.root875 line 4675
2825. lemma OAI.SharpPlanar.IntegerRoots.root875_contains line 4676
2826. def OAI.SharpPlanar.IntegerRoots.root876 line 4679
2827. lemma OAI.SharpPlanar.IntegerRoots.root876_contains line 4680
2828. def OAI.SharpPlanar.IntegerRoots.mid877 line 4683
2829. lemma OAI.SharpPlanar.IntegerRoots.mid877_contains line 4684
2830. def OAI.SharpPlanar.IntegerRoots.root877 line 4685
2831. lemma OAI.SharpPlanar.IntegerRoots.root877_contains line 4686
2832. def OAI.SharpPlanar.IntegerRoots.root878 line 4689
2833. lemma OAI.SharpPlanar.IntegerRoots.root878_contains line 4690
2834. def OAI.SharpPlanar.IntegerRoots.mid879 line 4693
2835. lemma OAI.SharpPlanar.IntegerRoots.mid879_contains line 4694
2836. def OAI.SharpPlanar.IntegerRoots.root879 line 4695
2837. lemma OAI.SharpPlanar.IntegerRoots.root879_contains line 4696
2838. def OAI.SharpPlanar.IntegerRoots.root880 line 4699
2839. lemma OAI.SharpPlanar.IntegerRoots.root880_contains line 4700
2840. def OAI.SharpPlanar.IntegerRoots.mid881 line 4703
2841. lemma OAI.SharpPlanar.IntegerRoots.mid881_contains line 4704
2842. def OAI.SharpPlanar.IntegerRoots.root881 line 4705
2843. lemma OAI.SharpPlanar.IntegerRoots.root881_contains line 4706
2844. def OAI.SharpPlanar.IntegerRoots.root882 line 4709
2845. lemma OAI.SharpPlanar.IntegerRoots.root882_contains line 4710
2846. def OAI.SharpPlanar.IntegerRoots.mid883 line 4713
2847. lemma OAI.SharpPlanar.IntegerRoots.mid883_contains line 4714
2848. def OAI.SharpPlanar.IntegerRoots.root883 line 4715
2849. lemma OAI.SharpPlanar.IntegerRoots.root883_contains line 4716
2850. def OAI.SharpPlanar.IntegerRoots.root884 line 4719
2851. lemma OAI.SharpPlanar.IntegerRoots.root884_contains line 4720
2852. def OAI.SharpPlanar.IntegerRoots.mid885 line 4723
2853. lemma OAI.SharpPlanar.IntegerRoots.mid885_contains line 4724
2854. def OAI.SharpPlanar.IntegerRoots.root885 line 4725
2855. lemma OAI.SharpPlanar.IntegerRoots.root885_contains line 4726
2856. def OAI.SharpPlanar.IntegerRoots.root886 line 4729
2857. lemma OAI.SharpPlanar.IntegerRoots.root886_contains line 4730
2858. def OAI.SharpPlanar.IntegerRoots.mid887 line 4733
2859. lemma OAI.SharpPlanar.IntegerRoots.mid887_contains line 4734
2860. def OAI.SharpPlanar.IntegerRoots.root887 line 4735
2861. lemma OAI.SharpPlanar.IntegerRoots.root887_contains line 4736
2862. def OAI.SharpPlanar.IntegerRoots.root888 line 4739
2863. lemma OAI.SharpPlanar.IntegerRoots.root888_contains line 4740
2864. def OAI.SharpPlanar.IntegerRoots.mid889 line 4743
2865. lemma OAI.SharpPlanar.IntegerRoots.mid889_contains line 4744
2866. def OAI.SharpPlanar.IntegerRoots.root889 line 4745
2867. lemma OAI.SharpPlanar.IntegerRoots.root889_contains line 4746
2868. def OAI.SharpPlanar.IntegerRoots.root890 line 4749
2869. lemma OAI.SharpPlanar.IntegerRoots.root890_contains line 4750
2870. def OAI.SharpPlanar.IntegerRoots.mid891 line 4753
2871. lemma OAI.SharpPlanar.IntegerRoots.mid891_contains line 4754
2872. def OAI.SharpPlanar.IntegerRoots.root891 line 4755
2873. lemma OAI.SharpPlanar.IntegerRoots.root891_contains line 4756
2874. def OAI.SharpPlanar.IntegerRoots.root892 line 4759
2875. lemma OAI.SharpPlanar.IntegerRoots.root892_contains line 4760
2876. def OAI.SharpPlanar.IntegerRoots.mid893 line 4763
2877. lemma OAI.SharpPlanar.IntegerRoots.mid893_contains line 4764
2878. def OAI.SharpPlanar.IntegerRoots.root893 line 4765
2879. lemma OAI.SharpPlanar.IntegerRoots.root893_contains line 4766
2880. def OAI.SharpPlanar.IntegerRoots.root894 line 4769
2881. lemma OAI.SharpPlanar.IntegerRoots.root894_contains line 4770
2882. def OAI.SharpPlanar.IntegerRoots.mid895 line 4773
2883. lemma OAI.SharpPlanar.IntegerRoots.mid895_contains line 4774
2884. def OAI.SharpPlanar.IntegerRoots.root895 line 4775
2885. lemma OAI.SharpPlanar.IntegerRoots.root895_contains line 4776
2886. def OAI.SharpPlanar.IntegerRoots.root896 line 4779
2887. lemma OAI.SharpPlanar.IntegerRoots.root896_contains line 4780
2888. def OAI.SharpPlanar.IntegerRoots.mid897 line 4783
2889. lemma OAI.SharpPlanar.IntegerRoots.mid897_contains line 4784
2890. def OAI.SharpPlanar.IntegerRoots.root897 line 4785
2891. lemma OAI.SharpPlanar.IntegerRoots.root897_contains line 4786
2892. def OAI.SharpPlanar.IntegerRoots.root898 line 4789
2893. lemma OAI.SharpPlanar.IntegerRoots.root898_contains line 4790
2894. def OAI.SharpPlanar.IntegerRoots.mid899 line 4793
2895. lemma OAI.SharpPlanar.IntegerRoots.mid899_contains line 4794
2896. def OAI.SharpPlanar.IntegerRoots.root899 line 4795
2897. lemma OAI.SharpPlanar.IntegerRoots.root899_contains line 4796
2898. def OAI.SharpPlanar.IntegerRoots.root900 line 4799
2899. lemma OAI.SharpPlanar.IntegerRoots.root900_contains line 4800
2900. def OAI.SharpPlanar.IntegerRoots.mid901 line 4803
2901. lemma OAI.SharpPlanar.IntegerRoots.mid901_contains line 4804
2902. def OAI.SharpPlanar.IntegerRoots.root901 line 4805
2903. lemma OAI.SharpPlanar.IntegerRoots.root901_contains line 4806
2904. def OAI.SharpPlanar.IntegerRoots.root902 line 4809
2905. lemma OAI.SharpPlanar.IntegerRoots.root902_contains line 4810
2906. def OAI.SharpPlanar.IntegerRoots.mid903 line 4813
2907. lemma OAI.SharpPlanar.IntegerRoots.mid903_contains line 4814
2908. def OAI.SharpPlanar.IntegerRoots.root903 line 4815
2909. lemma OAI.SharpPlanar.IntegerRoots.root903_contains line 4816
2910. def OAI.SharpPlanar.IntegerRoots.root904 line 4819
2911. lemma OAI.SharpPlanar.IntegerRoots.root904_contains line 4820
2912. def OAI.SharpPlanar.IntegerRoots.mid905 line 4823
2913. lemma OAI.SharpPlanar.IntegerRoots.mid905_contains line 4824
2914. def OAI.SharpPlanar.IntegerRoots.root905 line 4825
2915. lemma OAI.SharpPlanar.IntegerRoots.root905_contains line 4826
2916. def OAI.SharpPlanar.IntegerRoots.root906 line 4829
2917. lemma OAI.SharpPlanar.IntegerRoots.root906_contains line 4830
2918. def OAI.SharpPlanar.IntegerRoots.mid907 line 4833
2919. lemma OAI.SharpPlanar.IntegerRoots.mid907_contains line 4834
2920. def OAI.SharpPlanar.IntegerRoots.root907 line 4835
2921. lemma OAI.SharpPlanar.IntegerRoots.root907_contains line 4836
2922. def OAI.SharpPlanar.IntegerRoots.root908 line 4839
2923. lemma OAI.SharpPlanar.IntegerRoots.root908_contains line 4840
2924. def OAI.SharpPlanar.IntegerRoots.mid909 line 4843
2925. lemma OAI.SharpPlanar.IntegerRoots.mid909_contains line 4844
2926. def OAI.SharpPlanar.IntegerRoots.root909 line 4845
2927. lemma OAI.SharpPlanar.IntegerRoots.root909_contains line 4846
2928. def OAI.SharpPlanar.IntegerRoots.root910 line 4849
2929. lemma OAI.SharpPlanar.IntegerRoots.root910_contains line 4850
2930. def OAI.SharpPlanar.IntegerRoots.mid911 line 4853
2931. lemma OAI.SharpPlanar.IntegerRoots.mid911_contains line 4854
2932. def OAI.SharpPlanar.IntegerRoots.root911 line 4855
2933. lemma OAI.SharpPlanar.IntegerRoots.root911_contains line 4856
2934. def OAI.SharpPlanar.IntegerRoots.root912 line 4859
2935. lemma OAI.SharpPlanar.IntegerRoots.root912_contains line 4860
2936. def OAI.SharpPlanar.IntegerRoots.mid913 line 4863
2937. lemma OAI.SharpPlanar.IntegerRoots.mid913_contains line 4864
2938. def OAI.SharpPlanar.IntegerRoots.root913 line 4865
2939. lemma OAI.SharpPlanar.IntegerRoots.root913_contains line 4866
2940. def OAI.SharpPlanar.IntegerRoots.root914 line 4869
2941. lemma OAI.SharpPlanar.IntegerRoots.root914_contains line 4870
2942. def OAI.SharpPlanar.IntegerRoots.mid915 line 4873
2943. lemma OAI.SharpPlanar.IntegerRoots.mid915_contains line 4874
2944. def OAI.SharpPlanar.IntegerRoots.root915 line 4875
2945. lemma OAI.SharpPlanar.IntegerRoots.root915_contains line 4876
2946. def OAI.SharpPlanar.IntegerRoots.root916 line 4879
2947. lemma OAI.SharpPlanar.IntegerRoots.root916_contains line 4880
2948. def OAI.SharpPlanar.IntegerRoots.mid917 line 4883
2949. lemma OAI.SharpPlanar.IntegerRoots.mid917_contains line 4884
2950. def OAI.SharpPlanar.IntegerRoots.root917 line 4885
2951. lemma OAI.SharpPlanar.IntegerRoots.root917_contains line 4886
2952. def OAI.SharpPlanar.IntegerRoots.root918 line 4889
2953. lemma OAI.SharpPlanar.IntegerRoots.root918_contains line 4890
2954. def OAI.SharpPlanar.IntegerRoots.mid919 line 4893
2955. lemma OAI.SharpPlanar.IntegerRoots.mid919_contains line 4894
2956. def OAI.SharpPlanar.IntegerRoots.root919 line 4895
2957. lemma OAI.SharpPlanar.IntegerRoots.root919_contains line 4896
2958. def OAI.SharpPlanar.IntegerRoots.root920 line 4899
2959. lemma OAI.SharpPlanar.IntegerRoots.root920_contains line 4900
2960. def OAI.SharpPlanar.IntegerRoots.mid921 line 4903
2961. lemma OAI.SharpPlanar.IntegerRoots.mid921_contains line 4904
2962. def OAI.SharpPlanar.IntegerRoots.root921 line 4905
2963. lemma OAI.SharpPlanar.IntegerRoots.root921_contains line 4906
2964. def OAI.SharpPlanar.IntegerRoots.root922 line 4909
2965. lemma OAI.SharpPlanar.IntegerRoots.root922_contains line 4910
2966. def OAI.SharpPlanar.IntegerRoots.mid923 line 4913
2967. lemma OAI.SharpPlanar.IntegerRoots.mid923_contains line 4914
2968. def OAI.SharpPlanar.IntegerRoots.root923 line 4915
2969. lemma OAI.SharpPlanar.IntegerRoots.root923_contains line 4916
2970. def OAI.SharpPlanar.IntegerRoots.root924 line 4919
2971. lemma OAI.SharpPlanar.IntegerRoots.root924_contains line 4920
2972. def OAI.SharpPlanar.IntegerRoots.mid925 line 4923
2973. lemma OAI.SharpPlanar.IntegerRoots.mid925_contains line 4924
2974. def OAI.SharpPlanar.IntegerRoots.root925 line 4925
2975. lemma OAI.SharpPlanar.IntegerRoots.root925_contains line 4926
2976. def OAI.SharpPlanar.IntegerRoots.root926 line 4929
2977. lemma OAI.SharpPlanar.IntegerRoots.root926_contains line 4930
2978. def OAI.SharpPlanar.IntegerRoots.mid927 line 4933
2979. lemma OAI.SharpPlanar.IntegerRoots.mid927_contains line 4934
2980. def OAI.SharpPlanar.IntegerRoots.root927 line 4935
2981. lemma OAI.SharpPlanar.IntegerRoots.root927_contains line 4936
2982. def OAI.SharpPlanar.IntegerRoots.root928 line 4939
2983. lemma OAI.SharpPlanar.IntegerRoots.root928_contains line 4940
2984. def OAI.SharpPlanar.IntegerRoots.mid929 line 4943
2985. lemma OAI.SharpPlanar.IntegerRoots.mid929_contains line 4944
2986. def OAI.SharpPlanar.IntegerRoots.root929 line 4945
2987. lemma OAI.SharpPlanar.IntegerRoots.root929_contains line 4946
2988. def OAI.SharpPlanar.IntegerRoots.root930 line 4949
2989. lemma OAI.SharpPlanar.IntegerRoots.root930_contains line 4950
2990. def OAI.SharpPlanar.IntegerRoots.mid931 line 4953
2991. lemma OAI.SharpPlanar.IntegerRoots.mid931_contains line 4954
2992. def OAI.SharpPlanar.IntegerRoots.root931 line 4955
2993. lemma OAI.SharpPlanar.IntegerRoots.root931_contains line 4956
2994. def OAI.SharpPlanar.IntegerRoots.root932 line 4959
2995. lemma OAI.SharpPlanar.IntegerRoots.root932_contains line 4960
2996. def OAI.SharpPlanar.IntegerRoots.mid933 line 4963
2997. lemma OAI.SharpPlanar.IntegerRoots.mid933_contains line 4964
2998. def OAI.SharpPlanar.IntegerRoots.root933 line 4965
2999. lemma OAI.SharpPlanar.IntegerRoots.root933_contains line 4966
3000. def OAI.SharpPlanar.IntegerRoots.root934 line 4969
3001. lemma OAI.SharpPlanar.IntegerRoots.root934_contains line 4970
3002. def OAI.SharpPlanar.IntegerRoots.mid935 line 4973
3003. lemma OAI.SharpPlanar.IntegerRoots.mid935_contains line 4974
3004. def OAI.SharpPlanar.IntegerRoots.root935 line 4975
3005. lemma OAI.SharpPlanar.IntegerRoots.root935_contains line 4976
3006. def OAI.SharpPlanar.IntegerRoots.root936 line 4979
3007. lemma OAI.SharpPlanar.IntegerRoots.root936_contains line 4980
3008. def OAI.SharpPlanar.IntegerRoots.mid937 line 4983
3009. lemma OAI.SharpPlanar.IntegerRoots.mid937_contains line 4984
3010. def OAI.SharpPlanar.IntegerRoots.root937 line 4985
3011. lemma OAI.SharpPlanar.IntegerRoots.root937_contains line 4986
3012. def OAI.SharpPlanar.IntegerRoots.root938 line 4989
3013. lemma OAI.SharpPlanar.IntegerRoots.root938_contains line 4990
3014. def OAI.SharpPlanar.IntegerRoots.mid939 line 4993
3015. lemma OAI.SharpPlanar.IntegerRoots.mid939_contains line 4994
3016. def OAI.SharpPlanar.IntegerRoots.root939 line 4995
3017. lemma OAI.SharpPlanar.IntegerRoots.root939_contains line 4996
3018. def OAI.SharpPlanar.IntegerRoots.root940 line 4999
3019. lemma OAI.SharpPlanar.IntegerRoots.root940_contains line 5000
3020. def OAI.SharpPlanar.IntegerRoots.mid941 line 5003
3021. lemma OAI.SharpPlanar.IntegerRoots.mid941_contains line 5004
3022. def OAI.SharpPlanar.IntegerRoots.root941 line 5005
3023. lemma OAI.SharpPlanar.IntegerRoots.root941_contains line 5006
3024. def OAI.SharpPlanar.IntegerRoots.root942 line 5009
3025. lemma OAI.SharpPlanar.IntegerRoots.root942_contains line 5010
3026. def OAI.SharpPlanar.IntegerRoots.mid943 line 5013
3027. lemma OAI.SharpPlanar.IntegerRoots.mid943_contains line 5014
3028. def OAI.SharpPlanar.IntegerRoots.root943 line 5015
3029. lemma OAI.SharpPlanar.IntegerRoots.root943_contains line 5016
3030. def OAI.SharpPlanar.IntegerRoots.root944 line 5019
3031. lemma OAI.SharpPlanar.IntegerRoots.root944_contains line 5020
3032. def OAI.SharpPlanar.IntegerRoots.mid945 line 5023
3033. lemma OAI.SharpPlanar.IntegerRoots.mid945_contains line 5024
3034. def OAI.SharpPlanar.IntegerRoots.root945 line 5025
3035. lemma OAI.SharpPlanar.IntegerRoots.root945_contains line 5026
3036. def OAI.SharpPlanar.IntegerRoots.root946 line 5029
3037. lemma OAI.SharpPlanar.IntegerRoots.root946_contains line 5030
3038. def OAI.SharpPlanar.IntegerRoots.mid947 line 5033
3039. lemma OAI.SharpPlanar.IntegerRoots.mid947_contains line 5034
3040. def OAI.SharpPlanar.IntegerRoots.root947 line 5035
3041. lemma OAI.SharpPlanar.IntegerRoots.root947_contains line 5036
3042. def OAI.SharpPlanar.IntegerRoots.root948 line 5039
3043. lemma OAI.SharpPlanar.IntegerRoots.root948_contains line 5040
3044. def OAI.SharpPlanar.IntegerRoots.mid949 line 5043
3045. lemma OAI.SharpPlanar.IntegerRoots.mid949_contains line 5044
3046. def OAI.SharpPlanar.IntegerRoots.root949 line 5045
3047. lemma OAI.SharpPlanar.IntegerRoots.root949_contains line 5046
3048. def OAI.SharpPlanar.IntegerRoots.root950 line 5049
3049. lemma OAI.SharpPlanar.IntegerRoots.root950_contains line 5050
3050. def OAI.SharpPlanar.IntegerRoots.mid951 line 5053
3051. lemma OAI.SharpPlanar.IntegerRoots.mid951_contains line 5054
3052. def OAI.SharpPlanar.IntegerRoots.root951 line 5055
3053. lemma OAI.SharpPlanar.IntegerRoots.root951_contains line 5056
3054. def OAI.SharpPlanar.IntegerRoots.root952 line 5059
3055. lemma OAI.SharpPlanar.IntegerRoots.root952_contains line 5060
3056. def OAI.SharpPlanar.IntegerRoots.mid953 line 5063
3057. lemma OAI.SharpPlanar.IntegerRoots.mid953_contains line 5064
3058. def OAI.SharpPlanar.IntegerRoots.root953 line 5065
3059. lemma OAI.SharpPlanar.IntegerRoots.root953_contains line 5066
3060. def OAI.SharpPlanar.IntegerRoots.root954 line 5069
3061. lemma OAI.SharpPlanar.IntegerRoots.root954_contains line 5070
3062. def OAI.SharpPlanar.IntegerRoots.mid955 line 5073
3063. lemma OAI.SharpPlanar.IntegerRoots.mid955_contains line 5074
3064. def OAI.SharpPlanar.IntegerRoots.root955 line 5075
3065. lemma OAI.SharpPlanar.IntegerRoots.root955_contains line 5076
3066. def OAI.SharpPlanar.IntegerRoots.root956 line 5079
3067. lemma OAI.SharpPlanar.IntegerRoots.root956_contains line 5080
3068. def OAI.SharpPlanar.IntegerRoots.mid957 line 5083
3069. lemma OAI.SharpPlanar.IntegerRoots.mid957_contains line 5084
3070. def OAI.SharpPlanar.IntegerRoots.root957 line 5085
3071. lemma OAI.SharpPlanar.IntegerRoots.root957_contains line 5086
3072. def OAI.SharpPlanar.IntegerRoots.root958 line 5089
3073. lemma OAI.SharpPlanar.IntegerRoots.root958_contains line 5090
3074. def OAI.SharpPlanar.IntegerRoots.mid959 line 5093
3075. lemma OAI.SharpPlanar.IntegerRoots.mid959_contains line 5094
3076. def OAI.SharpPlanar.IntegerRoots.root959 line 5095
3077. lemma OAI.SharpPlanar.IntegerRoots.root959_contains line 5096
3078. def OAI.SharpPlanar.IntegerRoots.root960 line 5099
3079. lemma OAI.SharpPlanar.IntegerRoots.root960_contains line 5100
3080. def OAI.SharpPlanar.IntegerRoots.mid961 line 5103
3081. lemma OAI.SharpPlanar.IntegerRoots.mid961_contains line 5104
3082. def OAI.SharpPlanar.IntegerRoots.root961 line 5105
3083. lemma OAI.SharpPlanar.IntegerRoots.root961_contains line 5106
3084. def OAI.SharpPlanar.IntegerRoots.root962 line 5109
3085. lemma OAI.SharpPlanar.IntegerRoots.root962_contains line 5110
3086. def OAI.SharpPlanar.IntegerRoots.mid963 line 5113
3087. lemma OAI.SharpPlanar.IntegerRoots.mid963_contains line 5114
3088. def OAI.SharpPlanar.IntegerRoots.root963 line 5115
3089. lemma OAI.SharpPlanar.IntegerRoots.root963_contains line 5116
3090. def OAI.SharpPlanar.IntegerRoots.root964 line 5119
3091. lemma OAI.SharpPlanar.IntegerRoots.root964_contains line 5120
3092. def OAI.SharpPlanar.IntegerRoots.mid965 line 5123
3093. lemma OAI.SharpPlanar.IntegerRoots.mid965_contains line 5124
3094. def OAI.SharpPlanar.IntegerRoots.root965 line 5125
3095. lemma OAI.SharpPlanar.IntegerRoots.root965_contains line 5126
3096. def OAI.SharpPlanar.IntegerRoots.root966 line 5129
3097. lemma OAI.SharpPlanar.IntegerRoots.root966_contains line 5130
3098. def OAI.SharpPlanar.IntegerRoots.mid967 line 5133
3099. lemma OAI.SharpPlanar.IntegerRoots.mid967_contains line 5134
3100. def OAI.SharpPlanar.IntegerRoots.root967 line 5135
3101. lemma OAI.SharpPlanar.IntegerRoots.root967_contains line 5136
3102. def OAI.SharpPlanar.IntegerRoots.root968 line 5139
3103. lemma OAI.SharpPlanar.IntegerRoots.root968_contains line 5140
3104. def OAI.SharpPlanar.IntegerRoots.mid969 line 5143
3105. lemma OAI.SharpPlanar.IntegerRoots.mid969_contains line 5144
3106. def OAI.SharpPlanar.IntegerRoots.root969 line 5145
3107. lemma OAI.SharpPlanar.IntegerRoots.root969_contains line 5146
3108. def OAI.SharpPlanar.IntegerRoots.root970 line 5149
3109. lemma OAI.SharpPlanar.IntegerRoots.root970_contains line 5150
3110. def OAI.SharpPlanar.IntegerRoots.mid971 line 5153
3111. lemma OAI.SharpPlanar.IntegerRoots.mid971_contains line 5154
3112. def OAI.SharpPlanar.IntegerRoots.root971 line 5155
3113. lemma OAI.SharpPlanar.IntegerRoots.root971_contains line 5156
3114. def OAI.SharpPlanar.IntegerRoots.root972 line 5159
3115. lemma OAI.SharpPlanar.IntegerRoots.root972_contains line 5160
3116. def OAI.SharpPlanar.IntegerRoots.mid973 line 5163
3117. lemma OAI.SharpPlanar.IntegerRoots.mid973_contains line 5164
3118. def OAI.SharpPlanar.IntegerRoots.root973 line 5165
3119. lemma OAI.SharpPlanar.IntegerRoots.root973_contains line 5166
3120. def OAI.SharpPlanar.IntegerRoots.root974 line 5169
3121. lemma OAI.SharpPlanar.IntegerRoots.root974_contains line 5170
3122. def OAI.SharpPlanar.IntegerRoots.mid975 line 5173
3123. lemma OAI.SharpPlanar.IntegerRoots.mid975_contains line 5174
3124. def OAI.SharpPlanar.IntegerRoots.root975 line 5175
3125. lemma OAI.SharpPlanar.IntegerRoots.root975_contains line 5176
3126. def OAI.SharpPlanar.IntegerRoots.root976 line 5179
3127. lemma OAI.SharpPlanar.IntegerRoots.root976_contains line 5180
3128. def OAI.SharpPlanar.IntegerRoots.mid977 line 5183
3129. lemma OAI.SharpPlanar.IntegerRoots.mid977_contains line 5184
3130. def OAI.SharpPlanar.IntegerRoots.root977 line 5185
3131. lemma OAI.SharpPlanar.IntegerRoots.root977_contains line 5186
3132. def OAI.SharpPlanar.IntegerRoots.root978 line 5189
3133. lemma OAI.SharpPlanar.IntegerRoots.root978_contains line 5190
3134. def OAI.SharpPlanar.IntegerRoots.mid979 line 5193
3135. lemma OAI.SharpPlanar.IntegerRoots.mid979_contains line 5194
3136. def OAI.SharpPlanar.IntegerRoots.root979 line 5195
3137. lemma OAI.SharpPlanar.IntegerRoots.root979_contains line 5196
3138. def OAI.SharpPlanar.IntegerRoots.root980 line 5199
3139. lemma OAI.SharpPlanar.IntegerRoots.root980_contains line 5200
3140. def OAI.SharpPlanar.IntegerRoots.mid981 line 5203
3141. lemma OAI.SharpPlanar.IntegerRoots.mid981_contains line 5204
3142. def OAI.SharpPlanar.IntegerRoots.root981 line 5205
3143. lemma OAI.SharpPlanar.IntegerRoots.root981_contains line 5206
3144. def OAI.SharpPlanar.IntegerRoots.root982 line 5209
3145. lemma OAI.SharpPlanar.IntegerRoots.root982_contains line 5210
3146. def OAI.SharpPlanar.IntegerRoots.mid983 line 5213
3147. lemma OAI.SharpPlanar.IntegerRoots.mid983_contains line 5214
3148. def OAI.SharpPlanar.IntegerRoots.root983 line 5215
3149. lemma OAI.SharpPlanar.IntegerRoots.root983_contains line 5216
3150. def OAI.SharpPlanar.IntegerRoots.root984 line 5219
3151. lemma OAI.SharpPlanar.IntegerRoots.root984_contains line 5220
3152. def OAI.SharpPlanar.IntegerRoots.mid985 line 5223
3153. lemma OAI.SharpPlanar.IntegerRoots.mid985_contains line 5224
3154. def OAI.SharpPlanar.IntegerRoots.root985 line 5225
3155. lemma OAI.SharpPlanar.IntegerRoots.root985_contains line 5226
3156. def OAI.SharpPlanar.IntegerRoots.root986 line 5229
3157. lemma OAI.SharpPlanar.IntegerRoots.root986_contains line 5230
3158. def OAI.SharpPlanar.IntegerRoots.mid987 line 5233
3159. lemma OAI.SharpPlanar.IntegerRoots.mid987_contains line 5234
3160. def OAI.SharpPlanar.IntegerRoots.root987 line 5235
3161. lemma OAI.SharpPlanar.IntegerRoots.root987_contains line 5236
3162. def OAI.SharpPlanar.IntegerRoots.root988 line 5239
3163. lemma OAI.SharpPlanar.IntegerRoots.root988_contains line 5240
3164. def OAI.SharpPlanar.IntegerRoots.mid989 line 5243
3165. lemma OAI.SharpPlanar.IntegerRoots.mid989_contains line 5244
3166. def OAI.SharpPlanar.IntegerRoots.root989 line 5245
3167. lemma OAI.SharpPlanar.IntegerRoots.root989_contains line 5246
3168. def OAI.SharpPlanar.IntegerRoots.root990 line 5249
3169. lemma OAI.SharpPlanar.IntegerRoots.root990_contains line 5250
3170. def OAI.SharpPlanar.IntegerRoots.mid991 line 5253
3171. lemma OAI.SharpPlanar.IntegerRoots.mid991_contains line 5254
3172. def OAI.SharpPlanar.IntegerRoots.root991 line 5255
3173. lemma OAI.SharpPlanar.IntegerRoots.root991_contains line 5256
3174. def OAI.SharpPlanar.IntegerRoots.root992 line 5259
3175. lemma OAI.SharpPlanar.IntegerRoots.root992_contains line 5260
3176. def OAI.SharpPlanar.IntegerRoots.mid993 line 5263
3177. lemma OAI.SharpPlanar.IntegerRoots.mid993_contains line 5264
3178. def OAI.SharpPlanar.IntegerRoots.root993 line 5265
3179. lemma OAI.SharpPlanar.IntegerRoots.root993_contains line 5266
3180. def OAI.SharpPlanar.IntegerRoots.root994 line 5269
3181. lemma OAI.SharpPlanar.IntegerRoots.root994_contains line 5270
3182. def OAI.SharpPlanar.IntegerRoots.mid995 line 5273
3183. lemma OAI.SharpPlanar.IntegerRoots.mid995_contains line 5274
3184. def OAI.SharpPlanar.IntegerRoots.root995 line 5275
3185. lemma OAI.SharpPlanar.IntegerRoots.root995_contains line 5276
3186. def OAI.SharpPlanar.IntegerRoots.root996 line 5279
3187. lemma OAI.SharpPlanar.IntegerRoots.root996_contains line 5280
3188. def OAI.SharpPlanar.IntegerRoots.mid997 line 5283
3189. lemma OAI.SharpPlanar.IntegerRoots.mid997_contains line 5284
3190. def OAI.SharpPlanar.IntegerRoots.root997 line 5285
3191. lemma OAI.SharpPlanar.IntegerRoots.root997_contains line 5286
3192. def OAI.SharpPlanar.IntegerRoots.root998 line 5289
3193. lemma OAI.SharpPlanar.IntegerRoots.root998_contains line 5290
3194. def OAI.SharpPlanar.IntegerRoots.mid999 line 5293
3195. lemma OAI.SharpPlanar.IntegerRoots.mid999_contains line 5294
3196. def OAI.SharpPlanar.IntegerRoots.root999 line 5295
3197. lemma OAI.SharpPlanar.IntegerRoots.root999_contains line 5296
3198. def OAI.SharpPlanar.IntegerRoots.root1000 line 5299
3199. lemma OAI.SharpPlanar.IntegerRoots.root1000_contains line 5300
3200. def OAI.SharpPlanar.IntegerRoots.mid1001 line 5303
3201. lemma OAI.SharpPlanar.IntegerRoots.mid1001_contains line 5304
3202. def OAI.SharpPlanar.IntegerRoots.root1001 line 5305
3203. lemma OAI.SharpPlanar.IntegerRoots.root1001_contains line 5306
3204. def OAI.SharpPlanar.IntegerRoots.root1002 line 5309
3205. lemma OAI.SharpPlanar.IntegerRoots.root1002_contains line 5310
3206. def OAI.SharpPlanar.IntegerRoots.mid1003 line 5313
3207. lemma OAI.SharpPlanar.IntegerRoots.mid1003_contains line 5314
3208. def OAI.SharpPlanar.IntegerRoots.root1003 line 5315
3209. lemma OAI.SharpPlanar.IntegerRoots.root1003_contains line 5316
3210. def OAI.SharpPlanar.IntegerRoots.root1004 line 5319
3211. lemma OAI.SharpPlanar.IntegerRoots.root1004_contains line 5320
3212. def OAI.SharpPlanar.IntegerRoots.mid1005 line 5323
3213. lemma OAI.SharpPlanar.IntegerRoots.mid1005_contains line 5324
3214. def OAI.SharpPlanar.IntegerRoots.root1005 line 5325
3215. lemma OAI.SharpPlanar.IntegerRoots.root1005_contains line 5326
3216. def OAI.SharpPlanar.IntegerRoots.root1006 line 5329
3217. lemma OAI.SharpPlanar.IntegerRoots.root1006_contains line 5330
3218. def OAI.SharpPlanar.IntegerRoots.mid1007 line 5333
3219. lemma OAI.SharpPlanar.IntegerRoots.mid1007_contains line 5334
3220. def OAI.SharpPlanar.IntegerRoots.root1007 line 5335
3221. lemma OAI.SharpPlanar.IntegerRoots.root1007_contains line 5336
3222. def OAI.SharpPlanar.IntegerRoots.root1008 line 5339
3223. lemma OAI.SharpPlanar.IntegerRoots.root1008_contains line 5340
3224. def OAI.SharpPlanar.IntegerRoots.mid1009 line 5343
3225. lemma OAI.SharpPlanar.IntegerRoots.mid1009_contains line 5344
3226. def OAI.SharpPlanar.IntegerRoots.root1009 line 5345
3227. lemma OAI.SharpPlanar.IntegerRoots.root1009_contains line 5346
3228. def OAI.SharpPlanar.IntegerRoots.root1010 line 5349
3229. lemma OAI.SharpPlanar.IntegerRoots.root1010_contains line 5350
3230. def OAI.SharpPlanar.IntegerRoots.mid1011 line 5353
3231. lemma OAI.SharpPlanar.IntegerRoots.mid1011_contains line 5354
3232. def OAI.SharpPlanar.IntegerRoots.root1011 line 5355
3233. lemma OAI.SharpPlanar.IntegerRoots.root1011_contains line 5356
3234. def OAI.SharpPlanar.IntegerRoots.root1012 line 5359
3235. lemma OAI.SharpPlanar.IntegerRoots.root1012_contains line 5360
3236. def OAI.SharpPlanar.IntegerRoots.mid1013 line 5363
3237. lemma OAI.SharpPlanar.IntegerRoots.mid1013_contains line 5364
3238. def OAI.SharpPlanar.IntegerRoots.root1013 line 5365
3239. lemma OAI.SharpPlanar.IntegerRoots.root1013_contains line 5366
3240. def OAI.SharpPlanar.IntegerRoots.root1014 line 5369
3241. lemma OAI.SharpPlanar.IntegerRoots.root1014_contains line 5370
3242. def OAI.SharpPlanar.IntegerRoots.mid1015 line 5373
3243. lemma OAI.SharpPlanar.IntegerRoots.mid1015_contains line 5374
3244. def OAI.SharpPlanar.IntegerRoots.root1015 line 5375
3245. lemma OAI.SharpPlanar.IntegerRoots.root1015_contains line 5376
3246. def OAI.SharpPlanar.IntegerRoots.root1016 line 5379
3247. lemma OAI.SharpPlanar.IntegerRoots.root1016_contains line 5380
3248. def OAI.SharpPlanar.IntegerRoots.mid1017 line 5383
3249. lemma OAI.SharpPlanar.IntegerRoots.mid1017_contains line 5384
3250. def OAI.SharpPlanar.IntegerRoots.root1017 line 5385
3251. lemma OAI.SharpPlanar.IntegerRoots.root1017_contains line 5386
3252. def OAI.SharpPlanar.IntegerRoots.root1018 line 5389
3253. lemma OAI.SharpPlanar.IntegerRoots.root1018_contains line 5390
3254. def OAI.SharpPlanar.IntegerRoots.mid1019 line 5393
3255. lemma OAI.SharpPlanar.IntegerRoots.mid1019_contains line 5394
3256. def OAI.SharpPlanar.IntegerRoots.root1019 line 5395
3257. lemma OAI.SharpPlanar.IntegerRoots.root1019_contains line 5396
3258. def OAI.SharpPlanar.IntegerRoots.root1020 line 5399
3259. lemma OAI.SharpPlanar.IntegerRoots.root1020_contains line 5400
3260. def OAI.SharpPlanar.IntegerRoots.mid1021 line 5403
3261. lemma OAI.SharpPlanar.IntegerRoots.mid1021_contains line 5404
3262. def OAI.SharpPlanar.IntegerRoots.root1021 line 5405
3263. lemma OAI.SharpPlanar.IntegerRoots.root1021_contains line 5406
3264. def OAI.SharpPlanar.IntegerRoots.root1022 line 5409
3265. lemma OAI.SharpPlanar.IntegerRoots.root1022_contains line 5410
3266. def OAI.SharpPlanar.IntegerRoots.mid1023 line 5413
3267. lemma OAI.SharpPlanar.IntegerRoots.mid1023_contains line 5414
3268. def OAI.SharpPlanar.IntegerRoots.root1023 line 5415
3269. lemma OAI.SharpPlanar.IntegerRoots.root1023_contains line 5416