def un.odd_d1

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

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

1300def un.odd_d1(v: Nat) -> {U.U32Nat.odd(1n+Nat.double(v)) == 1n : Nat}:
1301  match v:
1302    case 0n:
1303      {==}
1304    case 1n+ +p:
1305      un.odd_d1(p)