def small

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:86

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/natcmp.bend as NC

86def small(+t: Nat, +ht: {Nat.is_le(t, 1n) == True{} : Bool}) -> {C.fits(1n, t) == True{} : Bool}:
87  match t:
88    case 0n:
89      {==}
90    case 1n:
91      {==}
92    case 2n+ +q:
93      NC.absurd_tf({C.fits(1n, 2n+q) == True{} : Bool}, ht)