~/jendhub

def internal_double_ne_succ_double

bend-mathlib@0.8.1.0 · nat.bend:3803

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

3803def internal_double_ne_succ_double(a: Nat, b: Nat, e: {Nat.double(a) == 1n+Nat.double(b) : Nat}) -> Empty:
3804  match a b:
3805    case 0n _:
3806      zero_ne_succ(Nat.double(b))(e)
3807    case 1n+p 0n:
3808      succ_ne_zero(Nat.double(p))(succ_inj(1n+Nat.double(p), 0n, e))
3809    case 1n+p 1n+q:
3810      internal_double_ne_succ_double(p, q, succ_inj(Nat.double(p), 1n+Nat.double(q), succ_inj(1n+Nat.double(p), 2n+Nat.double(q), e)))

Uses (6)

Used by (1)