def bitw.ffs_le_fls.t

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

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

404def bitw.ffs_le_fls.t(m: Nat) -> {Nat.is_le(1n, A.bitw.fls.step(m, True{})) == True{} : Bool}:
405  match m:
406    case 0n:
407      {==}
408    case 1n+k:
409      {==}