Validity of modular subtraction in _jAdd and _modifiedJacobianDouble

As the EVM does not have a submod instruction, the functions _jAdd and _modifiedJacobianDouble use the following pattern several times.

assembly {
    if lt(a, b) {
        a := add(p, a)
    }
    let c := sub(a, b)
}

The assumption here is that $a$ and $b$ both satisfy $0\le a,b<p$, and the intention is to have c = (a - b) % p. If $0\le b\le a<p$, then $0\le a-b<p$ holds, so plain subtraction can be used. In the case $a<b$, it holds that $0<(a+p)-b<p$, so $(a+p)-b=(a-b)+p$ is the value needed for $c$.

We note that while the add instruction could overflow (as $p$ is a 256-bit number), as both add and sub are calculated modulo $2^{256}$, the end result for $c$ will still be correct.