This is one of the reasons why I have some problems to trust proofs of properties of natural numbers formalized in CIC : Are some people “proving” properties of natural numbers that are already assumed in order to define CIC ?
There are (at least) three proofs of the consistency of PA that are important:
The proof in ZFC, which proceeeds by just verifying that N is a model of PA.
The proof by Gentzen. Here consistency is proved in a much weaker theory than ZFC (but of course the theory is not included in PA).
The proof by Gödel using what is now called the Dialectica interpretation. This proof uses a completely different method than Gentzen's proof, but obtains the same result. It is also conducted in a weak system, but a different weak system than Gentzen's proof.
The consistently of PA isn't a magical result; it is a well studied theorem that is equivalent to a combinatorial problem that roughly states that there is always a strategy to win at the Hydra game (see Laurie Kirby and Jeff Paris. "Accessible independence results for Peano arithmetic"). (Turns out that it is the case that every strategy wins the Hydra game.)
The paper "Essential Incompleteness of Arithmetic Verified by Coq" isn't novel for its mathematical result. No one doubted that the consistency of PA could be deduced in Coq in principle. The only novel result of that paper is that such a deduction could be carried out in practice (arguably even this isn't all that novel of a result either).
I also want to point out that proving that PA is consistent doesn't by itself mean that there isn't a proof that PA is inconsistent. To go from the existence of a deduction of some sentence S in some formal system T to the claim that S is actually true relies the assumption that the formal system T is sound, and to go from the existence of a deduction of some sentence S in some formal system T to the claim that there is no deduction of ¬S in T relies the assumption that the formal system T is consistent. In our case S is the sentence that "PA is consistent" and T is Coq. I don't explicitly claim that Coq is consistent as a logic. Of course the same issue holds for deductions in ZFC; however mathematicians don't generally go around prefacing every mathematical paper with a note saying that "this result of our deduction is only true under the assumption that ZFC is sound", although perhaps we should. ;)
I personally think there are good reasons to believe Martin-Lof style type theory (which I mean to cover systems such as CIC) is consistent. If we believe that Coq is normalizing then of course we cannot provide arguments to the function defined as the second component of the value that denotes the proof of the consistency of PA. Otherwise we could execute said function and normalize it to produce a constructor of the empty type, and there are no such constructors. The argument that terms in type theory are normalizing and amounts to another combinatorial problem that is going to be equivalent to finding a winning strategy against a hydra that is even more difficult to slay than Kirby and Paris's hydra.
You can prove Martin-Lof type theory is consistent using ZFC, and you can prove CIC is consistent using ZFC with some large cardinal assumptions.