def zeros_v
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:58
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64next.bend as F64next
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
58def zeros_v(+x: F.F64, +y: F.F64) -> {F.zeros(x, y) == Bool.and(SF.is_zero(x), SF.is_zero(y)) : Bool}:
59 Equal.trans(Bool, Bool.and(F.is_zero(x), F.is_zero(y)), Bool.and(SF.is_zero(x), F.is_zero(y)), Bool.and(SF.is_zero(x), SF.is_zero(y)), Equal.cong(Bool, Bool, t => Bool.and(t, F.is_zero(y)), F.is_zero(x), SF.is_zero(x), FB.is_zero_value(x)), Equal.cong(Bool, Bool, t => Bool.and(SF.is_zero(x), t), F.is_zero(y), SF.is_zero(y), FB.is_zero_value(y)))