def shc

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:147

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

147def shc(+e: Nat, +t: Nat, +N0: Nat, +h: {Nat.is_le(t, 1n+e) == True{} : Bool}) -> {C.shift(Nat.sub(1n+e, t), C.shift(t, N0)) == C.shift(1n+e, N0) : Nat}:
148  +es = Equal.trans(Nat, Nat.add(Nat.sub(1n+e, t), t), Nat.add(t, Nat.sub(1n+e, t)), 1n+e, NA.add_comm(Nat.sub(1n+e, t), t), N.sub_add(1n+e, t, h))
149  Equal.trans(Nat, C.shift(Nat.sub(1n+e, t), C.shift(t, N0)), C.shift(Nat.add(Nat.sub(1n+e, t), t), N0), C.shift(1n+e, N0), Equal.sym(Nat, C.shift(Nat.add(Nat.sub(1n+e, t), t), N0), C.shift(Nat.sub(1n+e, t), C.shift(t, N0)), WW.shift_comp(Nat.sub(1n+e, t), t, N0)), Equal.cong(Nat, Nat, u => C.shift(u, N0), Nat.add(Nat.sub(1n+e, t), t), 1n+e, es))