[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] How to search for a lemma?
Hello,
I _hate_ REAL_1 and REAL_2, I can never find anything in it.
I'm really looking forward to XREAL.
I just spent an hour looking for a lemma that would give me
for x,y being real number st x < y holds y - x > 0
Finally I gave up and used REAL_1:54 and REAL_1:36 with an
intermediate step (y - x > x - x).
So my question is not so much what was the lemma that I
needed, but how to find it myself. Grzegorz (or someone else
who knows), can you tell me how to do this with MML Query?
Freek