def ok_zy

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:515

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

515# what a false rbad says
516def ok_zy(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}) -> {SF.is_zero(y) == False{} : Bool}:
517  FC.or_r(Bool.or(Bool.not(SF.ordered(x, y)), SF.is_inf(x)), SF.is_zero(y), h)