def half_inv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/montnat.bend:34

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR

34# x == 2 x (m + 1) / 2 (mod m)
35def half_inv(+bp: Nat, +hh: Nat, +hM: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +x: Nat) -> {Nat.mod(x, 1n+bp) == Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp) : Nat}:
36  Equal.trans(Nat, Nat.mod(x, 1n+bp), Nat.mod(Nat.add(Nat.mul(x, 1n+bp), x), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(x, 1n+bp), x), 1n+bp), Nat.mod(x, 1n+bp), NR.absorb(bp, x, x)), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(x, 1n+bp), x), 1n+bp), Nat.mod(Nat.mul(x, 1n+1n+bp), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(x, 1n+bp), x), Nat.mul(x, 1n+1n+bp), Equal.trans(Nat, Nat.add(Nat.mul(x, 1n+bp), x), Nat.add(x, Nat.mul(x, 1n+bp)), Nat.mul(x, 1n+1n+bp), NA.add_comm(Nat.mul(x, 1n+bp), x), Equal.sym(Nat, Nat.mul(x, 1n+1n+bp), Nat.add(x, Nat.mul(x, 1n+bp)), NA.mul_succ(x, 1n+bp)))), Equal.trans(Nat, Nat.mod(Nat.mul(x, 1n+1n+bp), 1n+bp), Nat.mod(Nat.mul(x, Nat.add(hh, hh)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(x, z), 1n+bp), 1n+1n+bp, Nat.add(hh, hh), hM), Equal.trans(Nat, Nat.mod(Nat.mul(x, Nat.add(hh, hh)), 1n+bp), Nat.mod(Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(x, Nat.add(hh, hh)), Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), NA.mul_add_left(x, hh, hh)), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), 1n+bp), Nat.mod(Nat.mul(Nat.add(x, x), hh), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), Nat.mul(Nat.add(x, x), hh), Equal.sym(Nat, Nat.mul(Nat.add(x, x), hh), Nat.add(Nat.mul(x, hh), Nat.mul(x, hh)), NA.mul_add_right(x, x, hh))), Equal.trans(Nat, Nat.mod(Nat.mul(Nat.add(x, x), hh), 1n+bp), Nat.mod(Nat.mul(Nat.double(x), hh), 1n+bp), Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(z, hh), 1n+bp), Nat.add(x, x), Nat.double(x), Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x))), Equal.sym(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.double(x), 1n+bp), hh), 1n+bp), Nat.mod(Nat.mul(Nat.double(x), hh), 1n+bp), NR.mod_mul_l(bp, Nat.double(x), hh))))))))