def rne_ub

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:436

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

436def rne_ub(+m: Nat) -> {Nat.is_le(SF.rne(m, 10n), Nat.add(C.high(10n, m), 1n)) == True{} : Bool}:
437  N.le_add_left(SF.b2n(Bool.or(Nat.is_lt(512n, C.low(10n, m)), Bool.and(Nat.is_eq(C.low(10n, m), 512n), Nat.is_eq(Nat.mod(C.high(10n, m), 2n), 1n)))), 1n, C.high(10n, m), b2n_le1(Bool.or(Nat.is_lt(512n, C.low(10n, m)), Bool.and(Nat.is_eq(C.low(10n, m), 512n), Nat.is_eq(Nat.mod(C.high(10n, m), 2n), 1n)))))