∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ℤ) (x : G), f (n • a + x) = f x + n • b