[isabelle] Counterexamples produced by arith method



Using isabelle2005/HOL

lemma "a~=0 ==> (a*a) div a <= (a::nat)"
 apply(arith)

gives

Counter example:
a * a div a = 2, a = 1


What has gone wrong there ?
Why do I get a counterexample that is none ?





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