Injectivity of pedersen-segment-scalar.
Theorem 5.4.1 in [ZPS:220.127.116.11] proves
the injectivity of the encoding function \langle\cdot\rangle,
which is pedersen-segment-scalar in our formalization.
Theorem 5.4.1 also proves bounds of that function,
which we prove in pedersen-segment-scalar-bound
and in pedersen-segment-scalar-not-zero-proof.
is defined via pedersen-segment-scalar-loop,
so we need to prove injectivity properties for the latter first.
The proof is explained in the comments in this file.