def low_fit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/width.bend:413

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/lib/logic.bend as L

413def low_fit(+k: Nat, +r: Nat, +hr: {C.fits(k, r) == True{} : Bool}) -> {C.low(k, r) == r : Nat}:
414  +e = Equal.trans(Nat, Nat.add(r, C.shift(k, 0n)), Nat.add(r, 0n), r, Equal.cong(Nat, Nat, t => Nat.add(r, t), C.shift(k, 0n), 0n, shift_zero(k)), N.add_zero(r))
415  L.subst(Nat, z => {C.low(k, z) == r : Nat}, Nat.add(r, C.shift(k, 0n)), r, e, low_u(k, r, 0n, hr))