*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Strange counter example given by arith*From*: Norbert Voelker <norbert at essex.ac.uk>*Date*: Thu, 11 May 2006 13:16:48 +0100*User-agent*: Thunderbird 1.5.0.2 (Windows/20060308)

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

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

**Follow-Ups**:

- Previous by Date: [isabelle] Isabelle around the world
- Next by Date: Re: [isabelle] Strange counter example given by arith
- Previous by Thread: [isabelle] Isabelle around the world
- Next by Thread: Re: [isabelle] Strange counter example given by arith
- Cl-isabelle-users May 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list