def sh_split

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

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/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

133# shift(a, p) = shift(m, shift(a - m, p)) for m <= a
134def sh_split(+a: Nat, +m: Nat, +p: Nat, +h: {Nat.is_le(m, a) == True{} : Bool}) -> {C.shift(a, p) == C.shift(m, C.shift(Nat.sub(a, m), p)) : Nat}:
135  Equal.trans(Nat, C.shift(a, p), C.shift(Nat.add(m, Nat.sub(a, m)), p), C.shift(m, C.shift(Nat.sub(a, m), p)), Equal.cong(Nat, Nat, z => C.shift(z, p), a, Nat.add(m, Nat.sub(a, m)), Equal.sym(Nat, Nat.add(m, Nat.sub(a, m)), a, N.sub_add(a, m, h))), WW.shift_comp(m, Nat.sub(a, m), p))