def high_comp

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:438

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

438def high_comp(+a: Nat, +b: Nat, +n: Nat) -> {C.high(Nat.add(b, a), n) == C.high(a, C.high(b, n)) : Nat}:
439  match b:
440    case 0n:
441      {==}
442    case 1n+ +p:
443      high_comp(a, p, C.half(n))