def mok_odd

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32mont.bend:252

import Base
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S

252def mok_odd(+bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +hok: {X.mont32_ok(m) == True{} : Bool}) -> {Nat.mod(1n+bp, 2n) == 1n : Nat}:
253  +h = Equal.trans(Bool, Nat.is_eq(Nat.mod(v(m), 2n), 1n), U32.is_eq(U32.and(m, 1), 1), True{}, Equal.sym(Bool, U32.is_eq(U32.and(m, 1), 1), Nat.is_eq(Nat.mod(v(m), 2n), 1n), LW.tests_odd(m)), W64S.and_l(U32.is_eq(U32.and(m, 1), 1), U32.is_eq(U32.mul(m, X.minv32(m)), 4294967295), hok))
254  Equal.trans(Nat, Nat.mod(1n+bp, 2n), Nat.mod(v(m), 2n), 1n, Equal.cong(Nat, Nat, z => Nat.mod(z, 2n), 1n+bp, v(m), Equal.sym(Nat, v(m), 1n+bp, hM)), N.eq_from_is_eq(Nat.mod(v(m), 2n), 1n, h))