def shift_sc

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:195

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/word.bend as WD

195def shift_sc(+k: Nat, +x: Nat) -> {C.shift(k, x) == WD.sc(k, x) : Nat}:
196  match k:
197    case 0n:
198      {==}
199    case 1n+ +p:
200      Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, x), WD.sc(p, x), shift_sc(p, x))