def ns.odd_even

bend-osdev-word64@0.1.1.0 · proof_shift.bend:116

import Base

116# 1 + 2a = 2b never holds; 2a = 2b gives a = b
117def ns.odd_even(a: Nat, b: Nat, e: {1n+Nat.double(a) == Nat.double(b) : Nat}) -> Empty:
118  match a b:
119    case _ 0n:
120      ns.sz(Nat.double(a), e)
121    case 0n 1n+ +q:
122      ns.sz(Nat.double(q), Equal.sym(Nat, 0n, 1n+Nat.double(q), ns.succ_inj(0n, 1n+Nat.double(q), e)))
123    case 1n+ +p 1n+ +q:
124      ns.odd_even(p, q, ns.succ_inj(1n+Nat.double(p), Nat.double(q), ns.succ_inj(2n+Nat.double(p), 1n+Nat.double(q), e)))