def bitw.popcount_le

bend-osdev-algo@0.1.0.0 · PROOF.bend:160

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

160def bitw.popcount_le(n: Nat, w: Word(n)) -> {Nat.is_le(A.bitw.popcount(n, w), n) == True{} : Bool}:
161  match n:
162    case 0n:
163      {==}
164    case 1n+ +p:
165      match w:
166        case WCon{True{}, t}:
167          bitw.popcount_le(p, t)
168        case WCon{False{}, +t}:
169          nat.le_succ(A.bitw.popcount(p, t), p, bitw.popcount_le(p, t))