def even_odd

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:351

import Base

351def even_odd(+a: Nat, +b: Nat, e: {Nat.double(a) == 1n+Nat.double(b) : Nat}) -> Empty:
352  match a b:
353    case 0n _:
354      zero_succ(Nat.double(b), e)
355    case 1n+p 0n:
356      succ_zero(Nat.double(p), succ_inj(1n+Nat.double(p), 0n, e))
357    case 1n+p 1n+q:
358      even_odd(p, q, succ_inj(Nat.double(p), 1n+Nat.double(q), succ_inj(1n+Nat.double(p), 2n+Nat.double(q), e)))