How can we show that for all $n$, $k$ elements of Naturals, with $n < k$, that $\text{PA} \vdash \underline{n} < \underline{k}$?
This is the idea of formal consequences.
Also, For all $k$ in Naturals, $\text{PA} \vdash (\forall x)[x \leq \underline{k} \to x = \underline{0} \lor x = \underline{1} \lor \cdots \lor x = \underline{k}]$.
Induction sounds good, but cannot see the trick
As a hint: you do not specifically need induction to prove this, it is all provable from $\text{PA}^-$, the set of axioms of a discrete ordered semiring, which are shown on the Wikipedia article at http://en.wikipedia.org/wiki/Peano_axioms#Equivalent_axiomatizations .
Moreover, because both statements quantify over the standard naturals, there is no way to prove them by induction inside PA - if that worked, it would prove the result even for nonstandard elements of nonstandard models, but the result does not hold for them because they do not even have terms to represent them. So if you do use induction, it will have to be induction outside PA on the set of standard naturals.
Here is an example of the latter technique, which can be called "metainduction", applied to the first proposition in the question: for all $k,x \in \omega$ with $x < k$, $\text{PA}^-$ proves $\underline{x}<\underline{k}$. There is no natural number less than $0$, so the base case of the metainduction on $k$ will be trivial.
Now assume that $k \in \omega$ is fixed and $\text{PA}^-$ proves, for each $x \in \omega$ with $x < k$, that $\underline{x} < \underline{k}$. Suppose I am given $y \in \omega$ with $y < k+1$. If $y < k$, then $\text{PA}^-$ proves $\underline{y}<\underline{k}$; since $\text{PA}^-$ proves $\underline{k}<\underline{k+1}$ and proves that $<$ is transitive, $\text{PA}^-$ proves $\underline{y}<\underline{k+1}$. Otherwise $y = k$, and $\text{PA}^-$ proves directly that $\underline{k} < \underline{k+1}$. This gives us the inductive step we need; so for all $y,k \in \omega$ with $y < k$, $\text{PA}^-$ proves $\underline{y}<\underline{k}$. Note that induction in $\text{PA}^-$ was never used; in the inductive step we assume that certain formal proofs exist (e.g. that $\underline{y} < \underline{k}$) and we use them to create other formal proofs (that $\underline{y} < \underline{k+1}$).