def fits_hc
bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:135
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/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
135def fits_hc(+a: Nat, +b: Nat, +n: Nat) -> {C.fits(Nat.add(a, b), n) == C.fits(b, C.high(a, n)) : Bool}:
136 Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), C.high(Nat.add(a, b), n), C.high(b, C.high(a, n)), WW.high_comp(b, a, n))