Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] A simple lemma?

view this post on Zulip Email Gateway (Aug 19 2022 at 08:51):

From: John Munroe <munddr@gmail.com>
Hi,

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.

John

Last updated: Nov 21 2024 at 12:39 UTC