# Re: [isabelle] Nat theory proofs

Sorry, the 2 had type 'a.
Tim
________________________________
From: TIMOTHY KREMANN <twksoa262 at verizon.net>
To: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>
Sent: Wednesday, December 24, 2008 9:38:53 AM
Subject: Nat theory proofs
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

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