def half_div2

bend-collections-laws-math@1.0.0.0 · proofs/math/number/bitcount.bend:13

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

13def half_div2(+n: Nat) -> {C.half(n) == Nat.div(n, 2n) : Nat}:
14  match n:
15    case 0n:
16      {==}
17    case 1n:
18      {==}
19    case 2n+ +q:
20      Equal.trans(Nat, 1n+C.half(q), 1n+Nat.div(q, 2n), Nat.div(2n+q, 2n), Equal.cong(Nat, Nat, t => 1n+t, C.half(q), Nat.div(q, 2n), half_div2(q)), Equal.sym(Nat, Nat.div(2n+q, 2n), 1n+Nat.div(q, 2n), N.div2_step(q)))