[isabelle] Strange counter example given by arith



Trying to prove

   lemma div_less_square: "[| x < n * n; 0 < n |] ==> x div n < (n::nat)";

arith fails with the following counter example:

   x div n = 1, x  = 0, n * n = 1, n = 1

This seems odd given that ((x div n) = (0 div 1) = 0) according to Divides.div_0.

Any thoughts? Is my interpretation of the counter example perhaps incorrect?

Norbert.












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