def AP.dpos

bend-osdev-array@0.1.0.1 · PROOF.bend:783

import Base

783def AP.dpos(x: Nat, e: {Nat.is_lt(0n, x) == True{} : Bool}) -> {Nat.is_le(1n, Nat.double(x)) == True{} : Bool}:
784  match x:
785    case 0n:
786      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, AP.ft(e))
787    case 1n+y:
788      {==}