def eqc

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:52

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

52def eqc(+x: F.F64, +y: F.F64, +u: {Bool.or(SF.is_nan(x), SF.is_nan(y)) == False{} : Bool}) -> {F.eq(x, y) == Cmp.is_eq(SF.ord(x, y)) : Bool}:
53  Equal.trans(Bool, F.eq(x, y), Bool.and(Bool.not(Bool.or(SF.is_nan(x), SF.is_nan(y))), Cmp.is_eq(SF.ord(x, y))), Cmp.is_eq(SF.ord(x, y)), FC.eq_value(x, y), Equal.cong(Bool, Bool, b => Bool.and(Bool.not(b), Cmp.is_eq(SF.ord(x, y))), Bool.or(SF.is_nan(x), SF.is_nan(y)), False{}, u))