def chh
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:209
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as W64add
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/u32half.bend as UH
209def chh(+n: Nat) -> {C.half(n) == UH.hlf(n) : Nat}:
210 match n:
211 case 0n:
212 {==}
213 case 1n:
214 {==}
215 case 2n+ +q:
216 Equal.cong(Nat, Nat, t => 1n+t, C.half(q), UH.hlf(q), chh(q))