∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (x y : Mᵃᵒᵖ),
  (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) (x + y) =
    (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) x + (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) y