n : PosNum
⊢ decodePosNum (encodePosNum n) = n
⊢ ∀ (n : PosNum), decodePosNum (encodePosNum n) = n
intro n
case one

⊢ (if [] = [] then PosNum.one else PosNum.bit1 (decodePosNum [])) = PosNum.one

case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 (decodePosNum (encodePosNum m))) = PosNum.bit1 m

case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ PosNum.bit0 (decodePosNum (encodePosNum m)) = PosNum.bit0 m
n : PosNum
⊢ decodePosNum (encodePosNum n) = n
induction' n with m hm m hm <;> unfold encodePosNum decodePosNum
no goals
case one

⊢ (if [] = [] then PosNum.one else PosNum.bit1 (decodePosNum [])) = PosNum.one
rfl
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 m) = PosNum.bit1 m
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 (decodePosNum (encodePosNum m))) = PosNum.bit1 m
rw [hm]
no goals
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else PosNum.bit1 m) = PosNum.bit1 m
exact if_neg (encodePosNum_nonempty m)
no goals
case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ PosNum.bit0 (decodePosNum (encodePosNum m)) = PosNum.bit0 m
exact congr_arg PosNum.bit0 hm