def shift_eq0

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

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

262def shift_eq0(+k: Nat, +y: Nat) -> {Nat.is_eq(C.shift(k, y), 0n) == Nat.is_eq(y, 0n) : Bool}:
263  match k:
264    case 0n:
265      {==}
266    case 1n+ +p:
267      Equal.trans(Bool, Nat.is_eq(Nat.double(C.shift(p, y)), 0n), Nat.is_eq(C.shift(p, y), 0n), Nat.is_eq(y, 0n), dbl_eq0(C.shift(p, y)), shift_eq0(p, y))