it-plv/fiat-crypto/pull/333/files. // // Following the proof linked in the PR above, the changes are: // // 1. Negate [B] and [C] so they are positive. The invariant now involves a // subtraction. // 2. If step 2 (both [x] and [y] are even) runs, abort immediately. This // case needs to be handled by the caller. // 3. Subtract copies of [x] and [y] as needed in step 6 (both [u] and [v] // are odd) so coefficients stay in bounds. // 4. Replace the [u >= v] check with [u > v]. This changes the end...