English
If two values are distinct, then v(x) and v(y) yield the maximum on their sum: v(x+y) = max(v(x), v(y)) under the condition that v(x) ≠ v(y).
Русский
Если значения различны, то при суммировании выполняется v(x+y) = max(v(x), v(y)) при условии, что v(x) ≠ v(y).
LaTeX
$$$\\forall x,y\\;\\bigl(v(x) \\neq v(y)\\bigr) \\Rightarrow v(x+y) = \\max(v(x), v(y))$$$
Lean4
theorem map_add_of_distinct_val (h : v x ≠ v y) : v (x + y) = max (v x) (v y) :=
by
suffices ¬v (x + y) < max (v x) (v y) from or_iff_not_imp_right.1 (le_iff_eq_or_lt.1 (v.map_add x y)) this
intro h'
wlog vyx : v y < v x generalizing x y
· refine this h.symm ?_ (h.lt_or_gt.resolve_right vyx)
rwa [add_comm, max_comm]
rw [max_eq_left_of_lt vyx] at h'
apply lt_irrefl (v x)
calc
v x = v (x + y - y) := by simp
_ ≤ max (v <| x + y) (v y) := (map_sub _ _ _)
_ < v x := max_lt h' vyx
