def round0

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:339

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

339def round0(+xv: Nat) -> {SF.round(False{}, 0n, xv) == SF.zero(False{}) : F.F64}:
340  {==}