Injectivity of pedersen-segment-scalar.
Theorem 5.4.1 in [ZPS:5.4.1.7] 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.
Since pedersen-segment-scalar 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.
