*To*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Nat theory proofs*From*: TIMOTHY KREMANN <twksoa262 at verizon.net>*Date*: Wed, 24 Dec 2008 06:38:53 -0800 (PST)

I am trying to prove: lemma nataba: "\<forall> a b. (b::nat) < a --> a * a - (2 * b * a - b * b) = a * a - 2 * a * b + b * b" But Isabelle returns this text when I enter the above: proof (prove): step 0 goal (1 subgoal): 1. \<forall> a b. b < a --> a * a - (2 * b * a - b * b) = a * a - 2 * a * b + b * b Counterexample found: a = Suc (Suc (Suc 0)) b = Suc (Suc 0) Can someone explain to me how 1 = 1 is a counterexample? Thanks, Tim

**Follow-Ups**:**Re: [isabelle] Nat theory proofs***From:*Brian Huffman

- Previous by Date: [isabelle] Linear Arithmetic
- Next by Date: Re: [isabelle] Nat theory proofs
- Previous by Thread: [isabelle] Linear Arithmetic
- Next by Thread: Re: [isabelle] Nat theory proofs
- Cl-isabelle-users December 2008 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