def bit_le1

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

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

103def bit_le1(+n: Nat) -> {Nat.is_le(C.bit(n), 1n) == True{} : Bool}:
104  match n:
105    case 0n:
106      {==}
107    case 1n:
108      {==}
109    case 2n+ +q:
110      bit_le1(q)