[STATEMENT]
lemma iT_Plus_neg_Max: "
  \<lbrakk> finite I; I \<oplus>- k \<noteq> {} \<rbrakk> \<Longrightarrow> Max (I \<oplus>- k) = Max I - k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; I \<oplus>- k \<noteq> {}\<rbrakk> \<Longrightarrow> Max (I \<oplus>- k) = Max I - k
[PROOF STEP]
apply (simp add: iT_Plus_neg_image_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite I; I \<down>\<ge> k \<noteq> {}\<rbrakk> \<Longrightarrow> (MAX n\<in>I \<down>\<ge> k. n - k) = Max I - k
[PROOF STEP]
apply (simp add: Max_mono2 monoI cut_ge_finite cut_ge_Max_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done