def cmp_shift

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natcmp.bend:36

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

36def cmp_shift(+k: Nat, +a: Nat, +b: Nat) -> {Nat.cmp(C.shift(k, a), C.shift(k, b)) == Nat.cmp(a, b) : Cmp}:
37  match k:
38    case 0n:
39      {==}
40    case 1n+ +p:
41      Equal.trans(Cmp, Nat.cmp(Nat.double(C.shift(p, a)), Nat.double(C.shift(p, b))), Nat.cmp(C.shift(p, a), C.shift(p, b)), Nat.cmp(a, b), cmp_dbl(C.shift(p, a), C.shift(p, b)), cmp_shift(p, a, b))