def rne_cmp
bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:47
import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
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/proofs/math/typed/natcmp.bend as NC
47def rne_cmp(+q: Nat, +r: Nat, +h: Nat) -> {SF.rne_up(q, r, h) == rne_c(q, Nat.cmp(r, h)) : Nat}:
48 Equal.cong(Cmp, Nat, t => Nat.add(q, SF.b2n(Bool.or(Cmp.is_lt(t), Bool.and(Cmp.is_eq(Nat.cmp(r, h)), Nat.is_eq(Nat.mod(q, 2n), 1n))))), Nat.cmp(h, r), SF.flip(Nat.cmp(r, h)), Equal.sym(Cmp, SF.flip(Nat.cmp(r, h)), Nat.cmp(h, r), NC.cmp_flip(r, h)))