def le1

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

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

576def le1(+t: Nat, +h: {C.fits(1n, t) == True{} : Bool}) -> {Nat.is_le(t, 1n) == True{} : Bool}:
577  match t:
578    case 0n:
579      {==}
580    case 1n:
581      {==}
582    case 2n+ +p:
583      NC.absurd_tf({Nat.is_le(2n+p, 1n) == True{} : Bool}, h)