def bit_le_self

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

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/lib/nat.bend as N

190def bit_le_self(+n: Nat) -> {Nat.is_le(C.bit(n), n) == True{} : Bool}:
191  match n:
192    case 0n:
193      {==}
194    case 1n:
195      {==}
196    case 2n+ +q:
197      N.le_trans(C.bit(q), q, 2n+q, bit_le_self(q), N.le_trans(q, 1n+q, 2n+q, N.le_succ(q), N.le_succ(1n+q)))