~/jendhub

def fabs_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64close.bend:16

import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend as F64close
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/f64bits.bend as FB

16def fabs_v(+z: F.F64, +z2: F.F64, +h: {z == z2 : F.F64}) -> {F.abs(z) == SF.fabs(z2) : F.F64}:
17  Equal.trans(F.F64, F.abs(z), F.abs(z2), SF.fabs(z2), Equal.cong(F.F64, F.F64, t => F.abs(t), z, z2, h), FB.abs_value(z2))

Uses (6)

Used by (2)