def positive_double

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:322

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

322def positive_double(value: Nat,positive: {Nat.is_lt(0n,Nat.double(value)) == True{} : Bool}) -> {Nat.is_lt(0n,value) == True{} : Bool}:
323  match value:
324    case 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
325    case 1n+rest: {==}