def un.odd_d

bend-osdev-u32@0.1.0.0 · PROOF.bend:1293

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

1293def un.odd_d(v: Nat) -> {U.U32Nat.odd(Nat.double(v)) == 0n : Nat}:
1294  match v:
1295    case 0n:
1296      {==}
1297    case 1n+ +p:
1298      un.odd_d(p)