def div2

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsrel.bend:31

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/proofs/lib/nat.bend as N

31def div2(x: Nat) -> {Nat.div(x, 2n) == C.half(x) : Nat}:
32  match x:
33    case 0n:
34      {==}
35    case 1n:
36      {==}
37    case 2n+ +q:
38      %Equal.sym(Nat, Nat.div(Nat.add(2n, q), 2n), 1n+Nat.div(q, 2n), N.div2_step(q)) : {_ == 1n+C.half(q) : Nat}
39      Equal.cong(Nat, Nat, z => 1n+z, Nat.div(q, 2n), C.half(q), div2(q))