def ns.half_lt

bend-osdev-word64@0.1.1.0 · proof_shift.bend:171

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

171def ns.half_lt(x: Nat) -> {Nat.is_lt(x, 2n+Nat.double(U.U32Nat.half(x))) == True{} : Bool}:
172  match x:
173    case 0n:
174      {==}
175    case 1n+ +p:
176      match p:
177        case 0n:
178          {==}
179        case 1n+ +q:
180          ns.half_lt(q)