[STATEMENT]
lemma iprev_inext: "
  n \<noteq> Max I \<or> infinite I \<Longrightarrow> iprev (inext n I) I = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> Max I \<or> infinite I \<Longrightarrow> iprev (inext n I) I = n
[PROOF STEP]
by (blast intro: iprev_inext_infin iprev_inext_fin)