def sub_value
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addv.bend:156
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addv.bend as F64addv
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
156def sub_value(+x: F.F64, +y: F.F64) -> SF.Sub.value(x, y):
157 Equal.trans(F.F64, F.add(x, F.neg(y)), F.add(x, SF.neg(y)), SF.add(x, SF.neg(y)), Equal.cong(F.F64, F.F64, z => F.add(x, z), F.neg(y), SF.neg(y), FB.neg_value(y)), add_value(x, SF.neg(y)))