[isabelle] Proving a simple lemma



Hi all,

I'm trying to prove a simple lemma, but am stuck at the last proof step:

lemma test_wrong:
fixes f :: "real => real"
shows "(EX x y. fx ~= fy) --> ~(EX x y. fx > fy)"
apply (rule impI)
apply (rule notE)
apply auto

goal (1 subgoal):
1. !!(x::real) y::real. fx ~= fy --> False

I think I'm supposed to let x be y, but how do I do that in Isar? Also, is what I've done so far reasonable?

Thanks for the help.

Michael




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