[Hol-info] Proof related to REAL_BIGNUM

[Osman H. <o_...@en...>]

Hi HOL users,

I am trying to prove the following theorem in HOL

|- ?(n:num). !(r:real). r < & n

It is somewhat related to the REAL_BIGNUM theorem found in the realTheory:

|- !r. ?n. r < &n

and by looking at this REAL_BIGNUM theorem my goal seems provable: As for
every real number there exists a greater 'num' so there must be a 'num'
which is greater than the greatest real number.

I tried using quite a few different approaches but couldnt succeed so far
and the main bottleneck being the fact that the existential quantifier is
outside the universal one.

Any feedback/clues would be greatly appreciated.
Thanks and best regards,
--Osman