English
Adding the right vector after a left vector preserves a certain additivity at indices: append_add expresses a shelf of index-shift equalities.
Русский
При сложении левого вектора с правым вектором сохраняется определённая аддитивность по индексам; append_add задаёт равенства для сдвига индексов.
LaTeX
$$$ \forall {\ v},{\ w},{\ i}: \mathrm{append}(v,w)(i) = w(i) \text{ under appropriate indexing shifts.} $$$
Lean4
@[simp]
theorem append_add : ∀ {m} (v : Vector3 α m) {n} (w : Vector3 α n) (i : Fin2 n), (v +-+ w) (add i m) = w i
| 0, _, _, _, _ => rfl
| m + 1, v, n, w, i => v.consElim fun _a t => by simp [append_add, add]
