F64close.lek: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend as F64close
Lines 30-33 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend&start_line=30&end_line=33

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulv.bend as MV

# d <= |r * x| on the implementation is le_s against the spec's |r * x|
def lek(+d: F.F64, +r: F.F64, +x: F.F64) -> {F.le(d, F.abs(F.mul(r, x))) == SF.le_s(d, SF.fabs(SF.mul(r, x))) : Bool}:
  +R = SF.fabs(SF.mul(r, x))
  Equal.trans(Bool, F.le(d, F.abs(F.mul(r, x))), F.le(d, R), SF.le_s(d, R), Equal.cong(F.F64, Bool, t => F.le(d, t), F.abs(F.mul(r, x)), R, fabs_v(F.mul(r, x), SF.mul(r, x), MV.mul_value(r, x))), FC.le_value(d, R))

Uses (13):
  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.trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend&name=fabs_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&name=le_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulv.bend&name=mul_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=fabs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=le_s
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=abs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=mul