[isabelle] A simple theorem



Hi all,

Given


axiomatization
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.

John




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