def shift_add

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

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

170def shift_add(+k: Nat, +x: Nat, +y: Nat) -> {C.shift(k, Nat.add(x, y)) == Nat.add(C.shift(k, x), C.shift(k, y)) : Nat}:
171  match k:
172    case 0n:
173      {==}
174    case 1n+ +p:
175      Equal.trans(Nat, Nat.double(C.shift(p, Nat.add(x, y))), Nat.double(Nat.add(C.shift(p, x), C.shift(p, y))), Nat.add(Nat.double(C.shift(p, x)), Nat.double(C.shift(p, y))), Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, Nat.add(x, y)), Nat.add(C.shift(p, x), C.shift(p, y)), shift_add(p, x, y)), NA.double_add(C.shift(p, x), C.shift(p, y)))