| 0 | 0 | sup |
| 1 | 0 | lemma to!!== |
| 2 | 0 | prop lemma to negated double imply |
| 3 | 0 | prop lemma to negated and(1) |
| 4 | 0 | pred lemma addNegatedAll |
| 5 | 0 | pred lemma (A)to(~E~)(Imply) |
| 6 | 0 | pred lemma (E)to(~A~)(Imply) |
| 7 | 0 | pred lemma (E~)to(~A)(Imply) |
| 8 | 0 | pred lemma toNegatedAEA |
| 9 | 0 | lemma uniqueNegative |
| 10 | 0 | lemma doubleMinus |
| 11 | 0 | lemma minusNegated |
| 12 | 0 | lemma eqReflexivity |
| 13 | 0 | lemma eqSymmetry |
| 14 | 0 | lemma eqTransitivity |
| 15 | 0 | lemma eqTransitivity4 |
| 16 | 0 | lemma eqTransitivity5 |
| 17 | 0 | lemma eqTransitivity6 |
| 18 | 0 | lemma addEquations |
| 19 | 0 | lemma subtractEquations |
| 20 | 0 | lemma subtractEquationsLeft |
| 21 | 0 | lemma multiplyEquations |
| 22 | 0 | lemma eqNegated |
| 23 | 0 | lemma positiveToRight(Eq) |
| 24 | 0 | lemma positiveToLeft(Eq) |
| 25 | 0 | lemma positiveToLeft(Eq)(1 term) |
| 26 | 0 | lemma negativeToLeft(Eq) |
| 27 | 0 | lemma nonreciprocalToRight(Eq)(1 term) |
| 28 | 0 | lemma distributionOut(Minus) |
| 29 | 0 | lemma positiveToRight(Eq)(1 term) |
| 30 | 0 | lemma sameSeries(NumDiff) |
| 31 | 0 | lemma plusAssociativity(4 terms) |
| 32 | 0 | lemma lessNeq |
| 33 | 0 | lemma neqSymmetry |
| 34 | 0 | lemma neqNegated |
| 35 | 0 | lemma subNeqRight |
| 36 | 0 | lemma subNeqLeft |
| 37 | 0 | lemma negativeToRight(Neq)(1 term) |
| 38 | 0 | lemma neqAddition |
| 39 | 0 | lemma neqMultiplication |
| 40 | 0 | lemma nonzeroProduct(2) |
| 41 | 0 | lemma switchTerms(x<=y-z) |
| 42 | 0 | lemma negativeToLeft(Less)(1 term) |
| 43 | 0 | lemma +1IsPositive(N) |
| 44 | 0 | lemma (1/2)(x+y)-x=(1/2)(y-x) |
| 45 | 0 | lemma y-(1/2)(x+y)=(1/2)(y-x) |
| 46 | 0 | lemma expZero exact |
| 47 | 0 | lemma sameExp base |
| 48 | 0 | lemma sameExp indu |
| 49 | 0 | lemma sameExp |
| 50 | 0 | lemma exp(+1) |
| 51 | 0 | lemma positiveBase base |
| 52 | 0 | lemma positiveBase indu |
| 53 | 0 | lemma positiveBase |
| 54 | 0 | lemma base(1/2)Sum zero exact |
| 55 | 0 | lemma sameBase(1/2)Sum second base |
| 56 | 0 | lemma sameBase(1/2)Sum second indu |
| 57 | 0 | lemma sameBase(1/2)Sum second |
| 58 | 0 | lemma base(1/2)Sum(+1) |
| 59 | 0 | lemma base(1/2)Sum exact bound base |
| 60 | 0 | lemma base(1/2)Sum exact bound indu |
| 61 | 0 | lemma base(1/2)Sum exact bound |
| 62 | 0 | lemma base(1/2)Sum bound |
| 63 | 0 | lemma UStelescope zero exact |
| 64 | 0 | lemma sameTelescope second base |
| 65 | 0 | lemma sameTelescope second indu |
| 66 | 0 | lemma sameTelescope second |
| 67 | 0 | lemma UStelescope(+1) |
| 68 | 0 | lemma telescopeNumerical base |
| 69 | 0 | lemma telescopeNumerical indu |
| 70 | 0 | lemma telescopeNumerical |
| 71 | 0 | lemma telescopeBound base |
| 72 | 0 | lemma telescopeBound indu |
| 73 | 0 | lemma telescopeBound |
| 74 | 0 | lemma lessNeq(F) helper |
| 75 | 0 | lemma lessNeq(F) |
| 76 | 0 | lemma lessNeq(R) |
| 77 | 0 | lemma intervalSize base |
| 78 | 0 | lemma intervalSize indu |
| 79 | 0 | lemma intervalSize |
| 80 | 0 | lemma XSlessUS |
| 81 | 0 | lemma USdecreasing(+1) |
| 82 | 0 | lemma closeUS |
| 83 | 0 | lemma closeUS(n+1) |
| 84 | 0 | pred lemma allNegated(Imply) |
| 85 | 0 | pred lemma existNegated(Imply) |
| 86 | 0 | pred lemma intro exist helper |
| 87 | 0 | pred lemma intro exist |
| 88 | 0 | pred lemma exist mp |
| 89 | 0 | pred lemma exist mp2 |
| 90 | 0 | pred lemma 2exist mp |
| 91 | 0 | pred lemma 2exist mp2 |
| 92 | 0 | pred lemma EAE mp |
| 93 | 0 | pred lemma addAll |
| 94 | 0 | pred lemma addExist helper1 |
| 95 | 0 | pred lemma addExist helper2 |
| 96 | 0 | pred lemma addExist |
| 97 | 0 | pred lemma addExist(SimpleAnt) |
| 98 | 0 | pred lemma addExist(Simple) |
| 99 | 0 | pred lemma addEAE |
| 100 | 0 | pred lemma AEAnegated |
| 101 | 0 | pred lemma EEAnegated |
| 102 | 0 | lemma induction |
| 103 | 0 | lemma leqAntisymmetry |
| 104 | 0 | lemma leqTransitivity |
| 105 | 0 | lemma leqAddition |
| 106 | 0 | lemma leqMultiplication |
| 107 | 0 | lemma reciprocal |
| 108 | 0 | lemma equality |
| 109 | 0 | lemma eqLeq |
| 110 | 0 | lemma eqAddition |
| 111 | 0 | lemma eqMultiplication |
| 112 | 0 | lemma leqMultiplicationLeft |
| 113 | 0 | lemma leqLessEq |
| 114 | 0 | lemma lessLeq |
| 115 | 0 | lemma from leqGeq |
| 116 | 0 | lemma subLeqRight |
| 117 | 0 | lemma subLeqLeft |
| 118 | 0 | lemma leqPlus1 |
| 119 | 0 | lemma positiveToRight(Leq) |
| 120 | 0 | lemma positiveToRight(Leq)(1 term) |
| 121 | 0 | lemma negativeToRight(Leq) |
| 122 | 0 | lemma positiveToLeft(Leq) |
| 123 | 0 | lemma negativeToLeft(Leq) |
| 124 | 0 | lemma negativeToLeft(Leq)(1 term) |
| 125 | 0 | lemma leqAdditionLeft |
| 126 | 0 | lemma leqSubtraction |
| 127 | 0 | lemma leqSubtractionLeft |
| 128 | 0 | lemma thirdGeq |
| 129 | 0 | lemma leqNegated |
| 130 | 0 | lemma addEquations(Leq) |
| 131 | 0 | lemma multiplyEquations(Leq) |
| 132 | 0 | lemma thirdGeqSeries |
| 133 | 0 | lemma leqNeqLess |
| 134 | 0 | lemma fromLess |
| 135 | 0 | lemma toLess |
| 136 | 0 | lemma fromNotLess |
| 137 | 0 | lemma toNotLess |
| 138 | 0 | lemma negativeLessPositive |
| 139 | 0 | lemma leqLessTransitivity |
| 140 | 0 | lemma lessLeqTransitivity |
| 141 | 0 | lemma lessTransitivity |
| 142 | 0 | lemma lessTotality |
| 143 | 0 | lemma subLessRight |
| 144 | 0 | lemma subLessLeft |
| 145 | 0 |
lemma switchTerms(x |
| 146 | 0 |
lemma switchTerms(x-y |
| 147 | 0 | lemma lessAddition |
| 148 | 0 | lemma lessAdditionLeft |
| 149 | 0 | lemma lessMultiplication |
| 150 | 0 | lemma lessMultiplicationLeft |
| 151 | 0 | lemma lessDivision |
| 152 | 0 | lemma positiveToRight(Less) |
| 153 | 0 | lemma positiveToLeft(Less) |
| 154 | 0 | lemma negativeToLeft(Less) |
| 155 | 0 | lemma negativeToRight(Less) |
| 156 | 0 | lemma addEquations(Less) |
| 157 | 0 | lemma addEquations(LeqLess) |
| 158 | 0 | lemma reciprocalToLeft(Less) |
| 159 | 0 | lemma lessNegated |
| 160 | 0 | lemma positiveNonzero |
| 161 | 0 | lemma positiveNegated |
| 162 | 0 | lemma nonpositiveNegated |
| 163 | 0 | lemma negativeNegated |
| 164 | 0 | lemma nonnegativeNegated |
| 165 | 0 | lemma positiveHalved |
| 166 | 0 | lemma positiveInverted |
| 167 | 0 | lemma nonnegativeNumerical |
| 168 | 0 | lemma negativeNumerical |
| 169 | 0 | lemma positiveNumerical |
| 170 | 0 | lemma nonpositiveNumerical |
| 171 | 0 | lemma |0|=0 |
| 172 | 0 | lemma 0<=|x| |
| 173 | 0 | lemma x<=|x| |
| 174 | 0 | lemma fromPositiveNumerical |
| 175 | 0 | lemma sameNumerical |
| 176 | 0 | lemma signNumerical(+) |
| 177 | 0 | lemma signNumerical |
| 178 | 0 | lemma toNumericalLess |
| 179 | 0 | lemma fromNumericalGreater |
| 180 | 0 | lemma numericalDifference |
| 181 | 0 | lemma numericalDifferenceLess helper |
| 182 | 0 | lemma numericalDifferenceLess |
| 183 | 0 | lemma splitNumericalSumHelper |
| 184 | 0 | lemma splitNumericalSum(++) |
| 185 | 0 | lemma splitNumericalSum(--) |
| 186 | 0 | lemma splitNumericalSum(+-, smallNegative) |
| 187 | 0 | lemma splitNumericalSum(+-, bigNegative) |
| 188 | 0 | lemma splitNumericalSum(+-) |
| 189 | 0 | lemma splitNumericalSum(-+) |
| 190 | 0 | lemma splitNumericalSum |
| 191 | 0 | lemma splitNumericalProduct(++) |
| 192 | 0 | lemma splitNumericalProduct(+-) |
| 193 | 0 | lemma splitNumericalProduct |
| 194 | 0 | lemma insertMiddleTerm(Numerical) |
| 195 | 0 | lemma insertTwoMiddleTerms(Numerical) |
| 196 | 0 | lemma three2twoTerms |
| 197 | 0 | lemma three2threeTerms |
| 198 | 0 | lemma three2twoFactors |
| 199 | 0 | lemma three2threeFactors |
| 200 | 0 | lemma times(-1) |
| 201 | 0 | lemma times(-1)Left |
| 202 | 0 | lemma leqMax1 |
| 203 | 0 | lemma leqMax2 |
| 204 | 0 | lemma lessThanMax |
| 205 | 0 | lemma x+y=zBackwards |
| 206 | 0 | lemma x*y=zBackwards |
| 207 | 0 | lemma x=x+(y-y) |
| 208 | 0 | lemma x=x+y-y |
| 209 | 0 | lemma x=x*y*(1/y) |
| 210 | 0 | lemma insertMiddleTerm(Sum) |
| 211 | 0 | lemma insertTwoMiddleTerms(Sum) |
| 212 | 0 | lemma insertMiddleTerm(Difference) |
| 213 | 0 | lemma x*0+x=x |
| 214 | 0 | lemma x*0=0 |
| 215 | 0 | lemma nonnegativeFactors |
| 216 | 0 | lemma nonzeroFactors |
| 217 | 0 | lemma positiveFactors |
| 218 | 0 | lemma plusTimesMinus |
| 219 | 0 | lemma minusTimesMinus |
| 220 | 0 | lemma (-1)*(-1)+(-1)*1=0 |
| 221 | 0 | lemma (-1)*(-1)=1 |
| 222 | 0 | lemma 0<1Helper |
| 223 | 0 | lemma 0<1 |
| 224 | 0 | lemma 0<2 |
| 225 | 0 | lemma 0<3 |
| 226 | 0 | lemma 0<1/2 |
| 227 | 0 | lemma 0<1/3 |
| 228 | 0 | lemma x+x=2*x |
| 229 | 0 | lemma x+x+x=3*x |
| 230 | 0 | lemma (1/2)x+(1/2)x=x |
| 231 | 0 | lemma (1/3)x+(1/3)x+(1/3)x=x |
| 232 | 0 | lemma -x-y=-(x+y) |
| 233 | 0 | lemma -x*y=-(x*y) |
| 234 | 0 | lemma -0=0 |
| 235 | 0 | lemma sameFsymmetry |
| 236 | 0 | lemma sameFtransitivity |
| 237 | 0 | lemma f2R(Plus) |
| 238 | 0 | lemma f2R(Times) |
| 239 | 0 |
lemma < |
| 240 | 0 |
lemma < |
| 241 | 0 | lemma <<==Reflexivity |
| 242 | 0 | lemma <<==AntisymmetryHelper(Q) |
| 243 | 0 |
lemma fromNot |
| 244 | 0 |
lemma fromNot |
| 245 | 0 |
lemma fromNot |
| 246 | 0 |
lemma fromNot |
| 247 | 0 |
lemma fromNot |
| 248 | 0 | lemma fromNotSameF(Strongest) helper2 |
| 249 | 0 | lemma fromNotSameF(Strongest) helper |
| 250 | 0 | lemma fromNotSameF(Strongest) |
| 251 | 0 | lemma toLess(F) helper |
| 252 | 0 | lemma toLess(F) |
| 253 | 0 | lemma fromNot<< |
| 254 | 0 | lemma toLess(R) |
| 255 | 0 | lemma leqTotality(R) |
| 256 | 0 | lemma fromNotSameF(Weak)(Helper) |
| 257 | 0 | lemma fromNotSameF(Weak) |
| 258 | 0 | lemma fromNotLess(F) |
| 259 | 0 | lemma ==Addition |
| 260 | 0 | lemma ==AdditionLeft |
| 261 | 0 | lemma fpart-Bounded base |
| 262 | 0 | lemma fpart-Bounded indu helper |
| 263 | 0 | lemma fpart-Bounded indu |
| 264 | 0 | lemma fpart-Bounded |
| 265 | 0 | lemma f-Bounded helper |
| 266 | 0 | lemma f-Bounded |
| 267 | 0 | lemma sameFmultiplication helper |
| 268 | 0 | lemma sameFmultiplication |
| 269 | 0 | lemma eqMultiplication(R) |
| 270 | 0 | lemma eqMultiplicationLeft(R) |
| 271 | 0 | lemma x*0=0(F) |
| 272 | 0 | lemma x*0=0(R) |
| 273 | 0 | lemma lessMultiplication(F) helper2 |
| 274 | 0 | lemma lessMultiplication(F) helper |
| 275 | 0 | lemma lessMultiplication(F) |
| 276 | 0 | lemma lessMultiplication(R) |
| 277 | 0 | lemma leqMultiplication(R) |
| 278 | 0 | lemma plusAssociativity(F) |
| 279 | 0 | lemma plus0(F) |
| 280 | 0 | lemma plusCommutativity(F) |
| 281 | 0 | lemma timesAssociativity(F) |
| 282 | 0 | lemma times1f |
| 283 | 0 | lemma 2cauchy helper |
| 284 | 0 | lemma 2cauchy |
| 285 | 0 | lemma reciprocalF nonzero |
| 286 | 0 | lemma reciprocalFny nonzero |
| 287 | 0 | lemma eventually=f to sameF helper |
| 288 | 0 | lemma eventually=f to sameF |
| 289 | 0 | lemma fromNotSameF(Strong) helper2 |
| 290 | 0 | lemma fromNotSameF(Strong) helper |
| 291 | 0 | lemma fromNotSameF(Strong) |
| 292 | 0 | lemma sameFreciprocal helper |
| 293 | 0 | lemma sameFreciprocal |
| 294 | 0 | lemma from!!== |
| 295 | 0 | lemma reciprocal(R) |
| 296 | 0 | lemma timesCommutativity(F) |
| 297 | 0 | lemma distribution(F) |
| 298 | 0 | lemma fromMax(1) |
| 299 | 0 | lemma fromMax(2) |
| 300 | 0 | prop lemma to negated and |
| 301 | 0 | lemma positiveToRight(Less)(1 term) |
| 302 | 0 | pred lemma (A~)to(~E) |
| 303 | 0 | lemma ==Transitivity4 |
| 304 | 0 | lemma plus0Left(R) |
| 305 | 0 | lemma x=x+(y-y)(R) |
| 306 | 0 | lemma x=x+y-y(R) |
| 307 | 0 | lemma positiveToRight(Eq)(R) |
| 308 | 0 | lemma subtractEquations(R) |
| 309 | 0 | lemma neqAddition(R) |
| 310 | 0 | lemma eqAdditionLeft(R) |
| 311 | 0 | lemma three2twoTerms(R) |
| 312 | 0 | lemma positiveToRight(Less)(R) |
| 313 | 0 | lemma three2threeTerms(R) |
| 314 | 0 | lemma positiveToRight(Less)(1 term)(R) |
| 315 | 0 | lemma toLeq(Advanced)(R) |
| 316 | 0 | lemma leqNeqLess(R) |
| 317 | 0 | lemma subLeqLeft(R) |
| 318 | 0 | lemma leqLessTransitivity(R) |
| 319 | 0 | lemma negativeToLeft(Eq)(R) |
| 320 | 0 | lemma negativeToRight(Less)(R) |
| 321 | 0 | lemma !!==Symmetry |
| 322 | 0 | lemma negativeToRight(Eq)(R) |
| 323 | 0 | lemma negativeToRight(Eq)(1 term)(R) |
| 324 | 0 | lemma doubleMinus(R) |
| 325 | 0 | lemma uniqueNegative(R) |
| 326 | 0 | lemma subtractEquationsLeft(R) |
| 327 | 0 | lemma eqNegated(R) |
| 328 | 0 | lemma neqNegated(R) |
| 329 | 0 | lemma leqNegated(R) |
| 330 | 0 | lemma lessNegated(R) |
| 331 | 0 | lemma -0=0(R) |
| 332 | 0 | lemma negativeNegated(R) |
| 333 | 0 | lemma from leqGeq(R) |
| 334 | 0 | lemma subLeqRight(R) |
| 335 | 0 | lemma fromLess(R) |
| 336 | 0 | lemma nonnegativeNumerical(R) |
| 337 | 0 | lemma negativeNumerical(R) |
| 338 | 0 | lemma 0<=|x|(R) |
| 339 | 0 | lemma positiveNegated(R) |
| 340 | 0 | lemma addEquations(R) |
| 341 | 0 | lemma distributionOut(R) |
| 342 | 0 | lemma ==Transitivity5 |
| 343 | 0 | lemma x*0+x=x(R) |
| 344 | 0 | lemma x*0=0(R)fff |
| 345 | 0 | lemma times(-1)(R) |
| 346 | 0 | lemma times(-1)Left(R) |
| 347 | 0 | lemma -x-y=-(x+y)(R) |
| 348 | 0 | lemma lessTotality(R) |
| 349 | 0 | lemma positiveNumerical(R) |
| 350 | 0 | lemma signNumerical(+)(R) |
| 351 | 0 | lemma sameNumerical(R) |
| 352 | 0 | lemma minusNegated(R) |
| 353 | 0 | lemma signNumerical(R) |
| 354 | 0 | lemma numericalDifference(R) |
| 355 | 0 | lemma x<=|x|(R) |
| 356 | 0 | lemma USlimitIsUpperBound helper |
| 357 | 0 | lemma USlimitIsUpperBound |
| 358 | 0 | lemma (-1)*(-1)+(-1)*1=0(R) |
| 359 | 0 | lemma (-1)*(-1)=1(R) |
| 360 | 0 | lemma 0<1Helper(R) |
| 361 | 0 | lemma 0<1(R) |
| 362 | 0 | lemma expZero exact(R) |
| 363 | 0 | lemma positiveBase(R) base |
| 364 | 0 | lemma three2twoFactors(R) |
| 365 | 0 | lemma x=x*y*(1/y)(R) |
| 366 | 0 | lemma neqMultiplication(R) |
| 367 | 0 | lemma lessTransitivity(R) |
| 368 | 0 | lemma 0<2(R) |
| 369 | 0 | lemma sameExp(R) base |
| 370 | 0 | lemma sameExp(R) indu |
| 371 | 0 | lemma sameExp(R) |
| 372 | 0 | lemma subNeqLeft(R) |
| 373 | 0 | lemma subNeqRight(R) |
| 374 | 0 | lemma nonzeroFactors(R) |
| 375 | 0 | lemma nonnegativeFactors(R) |
| 376 | 0 | lemma positiveFactors(R) |
| 377 | 0 | lemma lessDivision(R) |
| 378 | 0 | lemma 0<1/2(R) |
| 379 | 0 | lemma positiveToRight(Eq)(1 term)(R) |
| 380 | 0 | lemma exp(+1)(R) |
| 381 | 0 | lemma positiveBase(R) indu |
| 382 | 0 | lemma positiveBase(R) |
| 383 | 0 | lemma -x*y=-(x*y)(R) |
| 384 | 0 | lemma positiveToLeft(Eq)(R) |
| 385 | 0 | lemma times1Left(R) |
| 386 | 0 | lemma ==Transitivity6 |
| 387 | 0 | lemma x+x=2*x(R) |
| 388 | 0 | lemma (1/2)x+(1/2)x=x(R) |
| 389 | 0 | lemma distributionOut(Minus)(R) |
| 390 | 0 | lemma (1/2)(x+y)-x=(1/2)(y-x)(R) |
| 391 | 0 | lemma intervalSize(R) base |
| 392 | 0 | lemma lessMultiplicationLeft(R) |
| 393 | 0 | lemma negativeToLeft(Less)(R) |
| 394 | 0 | lemma negativeToLeft(Less)(1 term)(R) |
| 395 | 0 | lemma y-(1/2)(x+y)=(1/2)(y-x)(R) |
| 396 | 0 | lemma intervalSize(R) indu |
| 397 | 0 | lemma intervalSize(R) |
| 398 | 0 | lemma XSlessUS(R) |
| 399 | 0 | lemma USdecreasing(+1)(R) |
| 400 | 0 | lemma expUnbounded base |
| 401 | 0 | lemma expUnbounded indu |
| 402 | 0 | lemma expUnbounded |
| 403 | 0 | lemma 1<=x+1(N) |
| 404 | 0 | lemma nonzeroProduct(2)(R) |
| 405 | 0 | lemma positiveNonzero(R) |
| 406 | 0 | lemma nonreciprocalToRight(Eq)(1 term)(R) |
| 407 | 0 | lemma expNonzero base |
| 408 | 0 | lemma expNonzero indu |
| 409 | 0 | lemma expNonzero |
| 410 | 0 | lemma expNonzero(2) |
| 411 | 0 | lemma multiplyEquations(R) |
| 412 | 0 | lemma halfBase base |
| 413 | 0 | lemma halfBase indu |
| 414 | 0 | lemma halfBase |
| 415 | 0 | lemma three2threeFactors(R) |
| 416 | 0 | lemma x*y=zBackwards(R) |
| 417 | 0 | lemma positiveInverted(R) |
| 418 | 0 | lemma reciprocalToRight(Less)(R) |
| 419 | 0 | lemma reciprocalToRight(Less)(1 term)(R) |
| 420 | 0 | lemma nonreciprocalToLeft(Less)(R) |
| 421 | 0 |
lemma 1 |
| 422 | 0 |
lemma switchFactors(1/x |
| 423 | 0 | lemma smallHalving |
| 424 | 0 | lemma intervalSize(anyPositive) |
| 425 | 0 | lemma USdecreasing(+n) base |
| 426 | 0 | lemma USdecreasing(+n) indu |
| 427 | 0 | lemma USdecreasing(+n) |
| 428 | 0 | lemma USdecreasing |
| 429 | 0 | lemma leqAdditionLeft(R) |
| 430 | 0 | lemma toNotLess(R) |
| 431 | 0 | lemma limitOfUSIsLeq |
| 432 | 0 | lemma subtractEquations(Less)(R) |
| 433 | 0 | lemma subtractEquationsLeft(Less)(R) |
| 434 | 0 | lemma lessNegated(Negative)(R) |
| 435 | 0 | prop lemma from negated and (imply) |
| 436 | 0 | prop lemma remove double neg (consequent) |
| 437 | 0 | lemma fromNotUpperBound |
| 438 | 0 | lemma distributionOut |
| 439 | 0 | lemma distributionOutLeft |
| 440 | 0 | lemma distributionLeft |
| 441 | 0 | lemma leqNUB |
| 442 | 0 | lemma USlimitIsLeastUpperBound helper |
| 443 | 0 | lemma USlimitIsLeastUpperBound |
| 444 | 0 | lemma fromNotLess(R) |
| 445 | 0 | pred lemma exist mp3 |
| 446 | 0 | lemma greaterPositive(N) |
| 447 | 0 | lemma ysFClose helper |
| 448 | 0 | lemma ysFClose |
| 449 | 0 | lemma ysFCauchy helper |
| 450 | 0 | lemma ysFCauchy |
| 451 | 0 | lemma cartProdIsRelation |
| 452 | 0 | lemma fromSubset |
| 453 | 0 | lemma subsetIsRelation |
| 454 | 0 | lemma toSeries |
| 455 | 0 | lemma fromSeries |
| 456 | 0 | lemma seriesSubsetCP |
| 457 | 0 | lemma valueType |
| 458 | 0 | prop lemma remove or |
| 459 | 0 | lemma fromSingleton |
| 460 | 0 | lemma inPair(1) |
| 461 | 0 | lemma inPair(2) |
| 462 | 0 | lemma sameMember(2) |
| 463 | 0 | lemma toBinaryUnion(1) |
| 464 | 0 | lemma toBinaryUnion(2) |
| 465 | 0 | lemma fromOrderedPair(twoLevels) |
| 466 | 0 | lemma toCartProd helper |
| 467 | 0 | lemma toCartProd |
| 468 | 0 | lemma nonreciprocalToRight(Eq) |
| 469 | 0 | lemma nonreciprocalToLeft(Eq)(1 term) |
| 470 | 0 | lemma sameReciprocal |
| 471 | 0 | lemma CPseparationIsRelation |
| 472 | 0 | lemma orderedPairEquality |
| 473 | 0 | lemma reciprocalIsFunction |
| 474 | 0 | lemma reciprocalIsTotal |
| 475 | 0 | lemma reciprocalIsRationalSeries |
| 476 | 0 | lemma crsIsRelation |
| 477 | 0 | lemma crsIsFunction |
| 478 | 0 | lemma crsIsTotal |
| 479 | 0 | lemma crsIsSeries |
| 480 | 0 | lemma crsLookup |
| 481 | 0 | lemma 0f |
| 482 | 0 | lemma 1f |
| 483 | 0 | lemma toSingleton |
| 484 | 0 | lemma fromSameSingleton |
| 485 | 0 | lemma singletonmembersEqual |
| 486 | 0 | lemma unequalsNotInSingleton |
| 487 | 0 | lemma nonsingletonmembersUnequal |
| 488 | 0 | lemma fromOrderedPair |
| 489 | 0 | lemma fromOrderedPair(1) |
| 490 | 0 | lemma fromOrderedPair(2) |
| 491 | 0 | lemma fromCartProd |
| 492 | 0 | lemma fromCartProd(1) |
| 493 | 0 | lemma fromCartProd(2) |
| 494 | 0 | lemma sameOrderedPair |
| 495 | 0 | lemma inSeries helper |
| 496 | 0 | lemma inSeries |
| 497 | 0 | lemma to=f subset helper |
| 498 | 0 | lemma to=f subset |
| 499 | 0 | lemma to=f |
| 500 | 0 | lemma productIsFunction |
| 501 | 0 | lemma productIsTotal |
| 502 | 0 | lemma productIsRationalSeries |
| 503 | 0 | lemma timesF |
| 504 | 0 | lemma -x+(1/2)x=-(1/2)x |
| 505 | 0 | lemma positiveTripled |
| 506 | 0 | lemma positiveDividedBy3 |
| 507 | 0 | lemma |x-x|=0 |
| 508 | 0 | lemma 1<2 |
| 509 | 0 | lemma 1/3<2/3 |
| 510 | 0 | lemma (1/3)x+(1/3)x=(2/3)x |
| 511 | 0 | lemma (2/3)x+(1/3)x=x |
| 512 | 0 | lemma -x+(2/3)x=-(1/3)x |
| 513 | 0 | lemma -(1/3)x-(1/3)x=-(2/3)x |
| 514 | 0 | lemma -x+(1/3)x=-(2/3)x |
| 515 | 0 | lemma preserveLessGreater |
| 516 | 0 | lemma closetolessIsLess |
| 517 | 0 | lemma subLessLeft(F) |
| 518 | 0 | lemma subLessLeft(R) |
| 519 | 0 | lemma closetogreaterIsGreater |
| 520 | 0 | lemma subLessRight(F) |
| 521 | 0 | lemma subLessRight(R) |
| 522 | 0 | tester1 |
| 523 | 0 | tester2 |
| 524 | 0 | tester3 |
| 525 | 0 | tester4 |
| 526 | 0 | tester5 |
| 527 | 0 | tester6 |
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,