have : Arith₁ (fun v => (f v).pos * (g v) + (f v).inv * (h v)) :=
  (add 0 1).comp₂ _
    ((mul 0 1).comp₂ _ ((pos 0).comp₁ _ hf) hg)
    ((mul 0 1).comp₂ _ ((inv 0).comp₁ _ hf) hh)
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
⊢ Arith₁ fun v => if 0 < f v then g v else h v
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
⊢ Arith₁ fun v => if 0 < f v then g v else h v