English
revAt distributes over addition: if n ≤ N and o ≤ O, then revAt(N+O)(n+o) = revAt N n + revAt O o.
Русский
revAt распределяется по сложению: если n ≤ N и o ≤ O, то revAt(N+O)(n+o) = revAt N n + revAt O o.
LaTeX
$$$\\forall N,O,n,o:\\; n \\le N \\land o \\le O \\Rightarrow \\mathrm{revAt}(N+O)(n+o) = \\mathrm{revAt}(N)n + \\mathrm{revAt}(O)o.$$$
Lean4
theorem revAt_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) : revAt (N + O) (n + o) = revAt N n + revAt O o :=
by
rcases Nat.le.dest hn with ⟨n', rfl⟩
rcases Nat.le.dest ho with ⟨o', rfl⟩
repeat' rw [revAt_le (le_add_right rfl.le)]
rw [add_assoc, add_left_comm n' o, ← add_assoc, revAt_le (le_add_right rfl.le)]
repeat' rw [add_tsub_cancel_left]
