def rone_c

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

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/lib/nat.bend as N

744def rone_c(+x: F.F64, +y: F.F64, +h: {SF.rbad(x, y) == False{} : Bool}, +hlt: {Nat.is_lt(SF.xexp(x), SF.xexp(y)) == True{} : Bool}, +o: Bool, +ho: {Nat.is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n) == o : Bool}) -> {F.rm_near(x, y, o) == RNs(x, y) : F.F64}:
745  match o:
746    case True{}:
747      rm_one(x, y, hlt, N.eq_from_is_eq(Nat.sub(F.dexp(y), F.dexp(x)), 1n, ho))
748    case False{}:
749      Equal.sym(F.F64, RNs(x, y), x, rm_many(x, y, hlt, ho, ok_fin(x, y, h)))