∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddCommGroup E] [inst_2 : PseudoMetricSpace E]
  (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) ≤ dist x y),
  SeminormedAddCommGroup.ofAddDist' h₁ h₂ =
    { toNorm := (SeminormedAddGroup.ofAddDist' h₁ h₂).toNorm,
      toAddGroup := (SeminormedAddGroup.ofAddDist' h₁ h₂).toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := (SeminormedAddGroup.ofAddDist' h₁ h₂).toPseudoMetricSpace, dist_eq := ⋯ }