Proving n + S n = S (n + n) without n + S m = S (n + m)

Is it possible to prove forall n, n + S n = S (n + n) (with or without induction) without using forall n m, n + S m = S (n + m)?

Looking at the proof, if I start by using induction on n, we end up in a state where the inductive hypothesis is too weak (similar to the problem of inducting on n for a given m):

n: nat
IHn: n + S n = S (n + n)
1/1
n + S (S n) = S (n + S n)

Solution

I have a perhaps boring answer: yes, by reducing the problem to forall n m, n + S m = S (n + m):

Goal forall n, n + S n = S (n + n).
Proof.
  intros n.
  generalize n at 2 4 as m.
(*
goal is now:
  n : nat
  ============================
  forall m : nat, n + S m = S (n + m)
*)
Abort.

However, I'm not sure this is what you were asking. Perhaps you want to know whether forall n, n + S n = S (n + n) implies forall n m, n + S m = S (n + m) in some weak theory where the latter is not outright provable. For example, we can ask whether forall n, P n n implies forall n m, P n m for a generic P, and then the answer is obviously "no". The answer then seems to depend on what you want to assume about addition and S. Their usual definitions are too strong for this problem because forall n m, n + S m = S (n + m) is already provable and anything implies a provable statement.