def jam_r1

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:337

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW

337def jam_r1(+q: Nat, +rp: Nat) -> {SW.jam(q, 1n+rp) == SW.jam(q, 1n) : Nat}:
338  Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(Nat.mod(q, 2n), z)), Nat.min(1n+rp, 1n), 1n, min1(rp))