{E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : Group E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y) → SeminormedGroup E