rw [addAlt, addAlt]
a b : Point
⊢ a.addAlt b = b.addAlt a
a b : Point
⊢ (match a, b with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }) =
    match b, a with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }