[STATEMENT]
lemma upper_max_interval[simp]: "upper (max_interval x y) = max (upper x) (upper y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper (max_interval x y) = max (upper x) (upper y)
[PROOF STEP]
by transfer auto