def q4

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbits.bend as Fixbits

import Base

108# 4 k
109def q4(k: Nat) -> Nat:
110  match k:
111    case 0n:
112      0n
113    case 1n+p:
114      Nat.add(4n, q4(p))

Uses (2)