[isabelle] Proving a simple lemma
I'm trying to prove a simple lemma, but am stuck at the last proof step:
fixes f :: "real => real"
shows "(EX x y. fx ~= fy) --> ~(EX x y. fx > fy)"
apply (rule impI)
apply (rule notE)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and