Daniel's answer is correct that the judgmental distinctness of $0$ and $\mathsf{succ}(m)$ is not what justifies a definition by pattern-matching. However, it is still a meaningful question of how to prove that $0$ and $\mathsf{succ}(m)$ are not judgmentally equal. (Stretching terminology a bit, Daniel answered your X and I'm going to answer your Y.)
Note that this is a metatheoretic question, in contrast to the internal proof that $0\neq \mathsf{succ}(m)$. Thus, even though judgmental equality implies typal equality, the answer to that question does not answer this one.
It's also worth noting that this is not a trivial question, even though $0$ and $\mathsf{succ}$ are distinct constructors. From an "algebraic" perspective on type theory, judgmental equality is just the smallest congruence generated by certain rules. Thus, two terms that don't "look" like they could possibly be equal might turn out to be equal by passing through some chain of forwards and backwards equalities to other terms.
For the same reason, it is a "global" question about the type theory, not one that can be answered by referring only to $\mathbb{N}$. For instance, in a higher inductive type such as the interval $\mathsf{I}$, with constructors $\mathsf{zero},\mathsf{one} : \mathsf{I}$ and $\mathsf{seg}:\mathsf{zero}=\mathsf{one}$, there is no "local" reason for $\mathsf{zero}$ and $\mathsf{one}$ to be judgmentally equal; but if the type theory also includes the equality reflection rule, then $\mathsf{seg}$ implies that $\mathsf{zero}\equiv\mathsf{one}$.
One answer to this question involves giving an algorithm for checking whether two terms are judgmentally equal. Probably the simplest such algorithm involves giving a "rewriting system" under which every term can be reduced to a "normal form", and then two terms are judgmentally equal if they reduce to the same normal form (up to $\alpha$-equivalence). Roughly speaking, this rewriting system consists of what the HoTT Book calls "computation rules". One then has to prove that this rewriting system is terminating, and that the relation of "reducing to the same normal form" is a congruence; thus it coincides with judgmental equality. Then one can simply observe that $0$ and $\mathsf{succ}(m)$ are (when $m$ is a variable) distinct normal forms.
In practice, nowadays more complicated algorithms are used. Among other reasons, this is in order to also include what the HoTT Book calls "uniqueness rules". These algorithms often go by names like "normalization by evaluation". The crucial idea is that there are two "phases" of the algorithm, one which applies the computational rewrites, and another which applies the uniqueness rules in the expansionary direction ($f \mapsto (\lambda x. f(x))$ or $u \mapsto (\pi_1(u),\pi_2(u))$) by inspecting their types. But the basic idea is the same: after proving that the algorithm is terminating and complete, we can run the algorithm on two terms to verify that they are unequal (or equal).
With that said, I don't know whether anyone has actually done this for Book HoTT. It's known for MLTT, on which Book HoTT is based, but Book HoTT adds not just axioms (which don't disrupt such an algorithm) to MLTT but new judgmental equalities (the computation rules for point-constructors of HITs), which then have to be incorporated in the algorithm. So (even laying aside the point that "Book HoTT" is not precisely specified because it is open-ended with respect to what HITs are definable) there may technically be an open question here. However, I think no type theorist who's familiar with such proofs would have much doubt that standard techniques ought to apply to Book HoTT (and it's possible that someone has already done it).
Edit: Simon has pointed out in the comments what I should clearly have realized myself, namely that another way to deduce that two terms are not judgmentally equal is to give a model in which they are interpreted by distinct things. Thus, for instance, the set-theoretic model proves this for MLTT, and the simplicial set model proves it for Book HoTT (modulo details in the construction of that model that aren't yet in the literature, such as showing that the univalent universes are closed under a sufficiently large class of higher inductive types).
