[isabelle] Natural property
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:
fixes a and b
assumes a1:"0<(a::nat)" and b1:"0<(b::nat)"
shows "\<exists>d c. a*d<b*c"
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
a * 1 < b * (a + 1)
I would demonstrate the thesis but I don't know how to do that.
Can anyone help me?
This archive was generated by a fusion of
Pipermail (Mailman edition) and