n : Num
⊢ decodeNum (encodeNum n) = n
⊢ ∀ (n : Num), decodeNum (encodeNum n) = n
intro n
case zero

⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero

case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n
n : Num
⊢ decodeNum (encodeNum n) = n
cases' n with n <;> unfold encodeNum decodeNum
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n
rw [decode_encodePosNum n]
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n
rw [PosNum.cast_to_num]
no goals
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n
exact if_neg (encodePosNum_nonempty n)
no goals
case zero

⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero
rfl