∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0) {c : NNReal},
  ‖f‖ ≤ ↑c → ‖SeparationQuotient.liftNormedAddGroupHom f hf‖ ≤ ↑c