∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E} {s : Set α},
  LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (Kf + Kg) (fun x => f x - g x) s