def le1

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:238

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

238def le1(+t: Nat, +h: {C.fits(1n, t) == True{} : Bool}) -> {Nat.is_le(t, 1n) == True{} : Bool}:
239  match t:
240    case 0n:
241      {==}
242    case 1n:
243      {==}
244    case 2n+ +p:
245      NC.absurd_tf({Nat.is_le(2n+p, 1n) == True{} : Bool}, h)