[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