F64fmod.shc: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as F64fmod
Lines 147-149 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend&start_line=147&end_line=149

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

def 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}:
  +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))
  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))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_comp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift