def jam1_m
bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:340
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as W64sh
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
340def jam1_m(+q: Nat, +rp: Nat) -> {SW.jam(q, 1n+rp) == 1n+Nat.double(C.half(q)) : Nat}:
341 Equal.trans(Nat, SW.jam(q, 1n+rp), SW.jam(q, 1n), 1n+Nat.double(C.half(q)), jam_r1(q, rp), jam1_k(q, Nat.mod(q, 2n), {==}, mod2_lt(q)))