Re: [isabelle] A simple theorem
Le Mardi 20 Septembre 2011 10:12:10 John Munroe a écrit :
> Hi all,
> c :: real and
> d :: real
> where ax1 : "c > 0"
> and ax2 : "d > 0"
> does anyone know how to prove
> lemma "c * d > 0"?
> It seems using the facts ax1 ax2 isn't sufficient.
> Thanks in Advance.
Invoking Sledgehammer (with command "sledgehammer") immediately gives a
by (metis ax1 ax2 real_mult_order)
which can then be rewritten:
by (simp add: real_mult_order[OF ax1 ax2])
by (rule real_mult_order[OF ax1 ax2])
This archive was generated by a fusion of
Pipermail (Mailman edition) and