def rne_lb
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:433
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round
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
433def rne_lb(+m: Nat) -> {Nat.is_le(C.high(10n, m), SF.rne(m, 10n)) == True{} : Bool}:
434 N.le_add_right(C.high(10n, m), 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)))))