def nfit_mono

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64light.bend:52

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

52def nfit_mono(+a: Nat, +b: Nat, +x: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +h: {C.fits(b, x) == False{} : Bool}) -> {C.fits(a, x) == False{} : Bool}:
53  nfit_mono_c(a, b, x, hab, h, C.fits(a, x), {==})