[STATEMENT]
lemma two_not_one: "2 \<noteq> (1::'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2::'a) \<noteq> (1::'a)
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
assume "2 = (1::'a)"
[PROOF STATE]
proof (state)
this:
(2::'a) = (1::'a)

goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
hence "2 - 1 = 1 - (1::'a)"
[PROOF STATE]
proof (prove)
using this:
(2::'a) = (1::'a)

goal (1 subgoal):
 1. (2::'a) - (1::'a) = (1::'a) - (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(2::'a) - (1::'a) = (1::'a) - (1::'a)

goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
hence "1 = (0::'a)"
[PROOF STATE]
proof (prove)
using this:
(2::'a) - (1::'a) = (1::'a) - (1::'a)

goal (1 subgoal):
 1. (1::'a) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1::'a) = (0::'a)

goal (1 subgoal):
 1. (2::'a) = (1::'a) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using one_neq_zero
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (0::'a)
(1::'a) \<noteq> (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed