[isabelle] 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.