[isabelle] A proof for existential

Hi all,

I've been stuck trying to find a proof for the following, could someone please shed some light?

f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y => hx > h y" and
ax2 :"EX x. (ALL y. x ~= y => hx > hy) => gx = 0"

lemma "EX x. gx = 0"

I've tried:

lemma "EX x. gx = 0"
using ax1 ax2
apply (intro exI)
apply (erule exE)+
apply (erule allE)
apply (erule impE)

which gives 2 subgoals, but they don't seem to be in the right direction...

Thanks for the help in advance.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.