Many books proves theorems by performing one proof step and using this step as a scheme they say by repeating this step $l$ times we prove that... I wonder whether there is some formal meta-theorem that says this is valid proof.
For example let's say I want to prove triangle inequality for multiple points (not only three) so I want to prove that $$ d(x_1, x_n) \le \sum_{x=1}^{n-1}d(x_i, x_{i+1}) $$
I already know that ordinal triangle inequality: $d(x_1, x_3) \le d(x_1, x_2) + d(x_2, x_3)$ holds.
Using this facts I can create perfectly formal proof for any constant $n$ that shows $$ d(x_1, x_2) + d(x_2, x_3) + d(x_3, x_4) + d(x_4, x_5) \ge d(x_1, x_2) + d(x_2, x_3) + d(x_3, x_5) $$
For arbitrary $n$ I could repeat this reasoning $n-3$ times so I have proof scheme for any arbitrary $n$ picked in advance. I would like to know whether there is some more or less generic meta-theorem that shows I can indeed iterate such proof step to get formal proof for any $n$. In other words is there a way to turn informal loop in proof scheme to some formal construct that would result in creating formal proof.
Any valid proof that can be expressed as "do something, then repeat until you're done" can be formalized as a proof by induction.
Why? Well, in order to make a proof by "repeat until you're done" into a valid proof, you have to show that you won't have to repeat forever - you'll eventually get done. That is, you should be able to assign some measure of complexity to all the situations that could arise as you repeat your proof step(s) and show that 1. each time you complete a step, you move to a strictly simpler situation, 2. if you ever arrive at a situation when you can't complete any more proof steps, you're done, and 3. the situation can't get strictly simpler infinitely many times in succession.
Condition 3 says that you want the relation "situation $x$ is simpler than situation $y$" to be well-founded, i.e. something you can do induction on.
Condition 2 says that you can handle the base cases (the proposition $P$ you're trying to prove is true there).
Condition 1 says that you can reduce the truth of $P$ at a situation $x$ to the truth of $P$ at some strictly simpler situation $y$ (by applying a proof step). Turning this around, we have the inductive condition: if $P$ is true at all situations $y$ which are strictly simpler than situation $x$, then $P$ is true at $x$.
If the measure of complexity is just a natural number, and a situation of complexity $n$ is simpler than a situation of complexity $m$ just when $n<m$, then you have normal mathematical induction (or maybe complete [or strong] induction). If the "simpler than" relation is a linear order, but with a different order-type than the order on $\mathbb{N}$, then you have transfinite induction. And if the relation is something weirder, then you have (most generally) well-founded induction.
But most cases that arise in practice, like the triangle inequality example you give, are just simple induction over the natural numbers rephrased. You're proving by induction on $n\geq 3$ that $$d(x_1,x_n) \leq \sum_{i = 1}^{n-1} d(x_i,x_{i+1}).$$ The measure of complexity is the number of terms in the sequence $x_1,\dots,x_n$.
The base case $n = 3$ is the triangle inequality. The inductive step follows exactly the argument you gave: applying the triangle inequality as $d(x_{n-2},x_n)\leq d(x_{n-2},x_{n-1}) + d(x_{n-1},x_n)$, we get $$d(x_1,x_2) + \dots + d(x_{n-2},x_n) \leq \sum_{i = 1}^{n-1}d(x_i,x_{i+1}).$$
And instead of saying "repeat", we can conclude by induction, since we've made the problem simpler. Now there are $n-1$ elements in the sequence $x_1,\dots,x_{n-2},x_n$, so $$d(x_1,x_n) \leq d(x_1,x_2) + \dots + d(x_{n-2},x_n)\leq \sum_{i = 1}^{n-1}d(x_i,x_{i+1}).$$