def ns.half_le

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

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

159# 2 * (x / 2) <= x < 2 + 2 * (x / 2)
160def ns.half_le(x: Nat) -> {Nat.is_le(Nat.double(U.U32Nat.half(x)), x) == True{} : Bool}:
161  match x:
162    case 0n:
163      {==}
164    case 1n+ +p:
165      match p:
166        case 0n:
167          {==}
168        case 1n+ +q:
169          ns.half_le(q)