∀ {α : Type u_2} {β : Type u_1} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] {p : ENNReal}
  (x y : WithLp p (α × β)), WithLp.toLp p (0, (x + y).snd) = WithLp.toLp p (0, x.snd) + WithLp.toLp p (0, y.snd)