def bit_small
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:95
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as F64round
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
95def bit_small(+t: Nat, +ht: {Nat.is_le(t, 1n) == True{} : Bool}) -> {C.bit(t) == t : Nat}:
96 match t:
97 case 0n:
98 {==}
99 case 1n:
100 {==}
101 case 2n+ +q:
102 NC.absurd_tf({C.bit(2n+q) == 2n+q : Nat}, ht)