[STATEMENT]
lemma delta_unique:
  assumes r: "F (dual r, r) = r"
  shows "r = delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta
[PROOF STEP]
unfolding delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta_pos
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<le> delta_pos
 2. delta_pos \<le> r
[PROOF STEP]
show "delta_pos \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos \<le> r
[PROOF STEP]
using assms delta_pos_neg_least[where rm=r and rp=r]
[PROOF STATE]
proof (prove)
using this:
F (dual r, r) = r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_neg \<le> dual r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_pos \<le> r

goal (1 subgoal):
 1. delta_pos \<le> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
delta_pos \<le> r

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
have "delta_neg \<le> dual r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_neg \<le> dual r
[PROOF STEP]
using assms delta_pos_neg_least[where rm=r and rp=r]
[PROOF STATE]
proof (prove)
using this:
F (dual r, r) = r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_neg \<le> dual r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_pos \<le> r

goal (1 subgoal):
 1. delta_neg \<le> dual r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
delta_neg \<le> dual r

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
delta_neg \<le> dual r
[PROOF STEP]
have "r \<le> undual delta_neg"
[PROOF STATE]
proof (prove)
using this:
delta_neg \<le> dual r

goal (1 subgoal):
 1. r \<le> undual delta_neg
[PROOF STEP]
by (simp add: less_eq_dual_def)
[PROOF STATE]
proof (state)
this:
r \<le> undual delta_neg

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<le> undual delta_neg
[PROOF STEP]
show "r \<le> delta_pos"
[PROOF STATE]
proof (prove)
using this:
r \<le> undual delta_neg

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
using delta_eq
[PROOF STATE]
proof (prove)
using this:
r \<le> undual delta_neg
undual delta_neg = delta_pos

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<le> delta_pos

goal:
No subgoals!
[PROOF STEP]
qed