~/jendhub

def high_half

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/shrn.bend:34

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as Shrn
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

34# high(p, half(n)) == half(high(p, n)): both halve p + 1 times
35def high_half(+p: Nat, +n: Nat) -> {C.high(p, C.half(n)) == C.half(C.high(p, n)) : Nat}:
36  match p:
37    case 0n:
38      {==}
39    case 1n+q:
40      high_half(q, C.half(n))

Uses (3)

Used by (1)