def hlf_div2

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/u32laws.bend:149

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend as UH

149def hlf_div2(+n: Nat) -> {UH.hlf(n) == Nat.div(n, 2n) : Nat}:
150  match n:
151    case 0n:
152      {==}
153    case 1n:
154      {==}
155    case 2n+ +q:
156      %Equal.sym(Nat, Nat.div(Nat.add(2n, q), 2n), 1n+Nat.div(q, 2n), N.div2_step(q)) : {1n+UH.hlf(q) == _ : Nat}
157      N.succ_cong(UH.hlf(q), Nat.div(q, 2n), hlf_div2(q))