[isabelle] Natural property



Hello,
I'm trying to write some simple proofs and in particular I want to
demonstrate the follow
ALL (a::nat) (b::nat). a>0 AND b>0 --> EXISTS c d. a*d<b*c
but I don't find the correct way.

I fixed 'a' and 'b' and assumed 'a>0' and 'b>0 ', now I want demonstrate the
EXISTS formulae showing that a possible instantiation of 'c' and 'd' is
respectively (a+1) and 1.

In each my effort I reach the error
empty result sequence -- proof command failed
and I don't know how resolve it.

This is my proof sketch:
lemma
fixes a and b
assumes a1:"0<(a::nat)" and b1:"0<(b::nat)"
shows "\<exists>d c. a*d<b*c"
proof -
 have a2: "a<(a+1)" by (arith)
 from b1 and Nat.Suc_leI have a3: "1<=b" by (simp)
 have a4: "(0::nat)<1" by (auto)
 have a5: "a*1<b*(a+1)"
   using a3 and a4 and a2 and a1 and b1 and
Ring_and_Field.mult_le_less_imp_less [where a="1" and b="b" and c="a" and
d="a+1"]
   by (simp)


Now from
a * 1 < b * (a + 1)
I would demonstrate the thesis but I don't know how to do that.

Can anyone help me?

Thanks




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