∀ {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M → N) (a b : M),
  (∀ (y : M), f (a + y) = f a + f y) → (∀ (y : M), f (b + y) = f b + f y) → ∀ (y : M), f (a + b + y) = f (a + b) + f y