[isabelle] A simple lemma?


I have the following fact

snd ((?g::real => 'a * 'b) (1::real)) < snd ((?f::real => 'a * 'b)
(1::real)) --> ?g < ?f

and I'm trying to prove

(%x::real. (x, 1::real)) < (%x::real. (x, 2::real))

but auto doesn't seem to be able to resolve it. The antecedent is easy
for auto, but somehow it can't resolve the lemma above. Could someone
please help?

Thanks a lot.


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