Sequencing or continuation-passing in pure lambda-calculus
I do not think you will find what you are looking for in the pure lambda calculus. The key is this statement you made:

A sequencing operator can also help to define the addition. If an application of a numeral |m| is delayed until a numeral |n| is applied to all its arguments, ...

Well, models of the lambda calculus are supposed to be like:
$$U \cong U^U$$
And the point of this is that every semantic value $u \in U$ may be applied to something. So it makes no sense to talk about something being &quot;applied to all its arguments.&quot; There is no value that cannot be applied to more arguments in the pure lambda calculus.
I don't know off hand of a model/argument that this representation of naturals makes it impossible to implement IsZero, although some thinking about it makes it seem unlikely. However, if it is to be possible in the pure lambda calculus, it will have to make sense semantically, and not be based on notions that are only syntactic.
Edit: here is a sketch of an argument. A definition of $\mathsf{IsZero}$ must eventually reduce like:
$$\mathsf{IsZero}\ n \rightsquigarrow^* n \overrightarrow v$$
The reason is that applying to some number of values is the only mechanism in the lambda calculus to actually distinguish between numerals. It needs to be the case that: $$0 \overrightarrow v = \mathsf{true} \\ \mathsf{s}n \overrightarrow v = \mathsf{false}$$ However, for every $\overrightarrow v$ it is the case that: $$||\overrightarrow v| + k|\overrightarrow v = |k|$$ (where $|\overrightarrow v|$ is the length of $\overrightarrow v$). But only $|1| = \mathsf{false}$ (if that is the convention chosen). In English, there is no bound on the number of terms required to get a boolean by applying a numeral. So there cannot be a $\overrightarrow v$ that satisfies the equations for all numerals, and thus $\mathsf{IsZero}$ cannot be defined.