def fits_up

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

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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

68def fits_up(+a: Nat, +d: Nat, +x: Nat, +h: {C.fits(a, x) == True{} : Bool}) -> {C.fits(Nat.add(a, d), x) == True{} : Bool}:
69  +e = N.eq_from_is_eq(C.high(a, x), 0n, h)
70  %Equal.sym(Nat, C.high(Nat.add(a, d), x), C.high(d, C.high(a, x)), WW.high_comp(d, a, x)) : {Nat.is_eq(_, 0n) == True{} : Bool}
71  %Equal.sym(Nat, C.high(a, x), 0n, e) : {Nat.is_eq(C.high(d, _), 0n) == True{} : Bool}
72  fits0(d)