∀ {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 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] [inst_5 : AddCommGroup H] [inst_6 : PartialOrder H]
  [IsOrderedAddMonoid H] [AddConstMapClass F G H a b] {f : F},
  0 < a → ∀ (l : G), Antitone ⇑f ↔ AntitoneOn (⇑f) (Set.Icc l (l + a))