case head

⊢ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } =
    ↑χ₄ ↑{ val := 0, isLt := (_ : 0 < 7 + 1) } * ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) }

case tail.head

⊢ ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } =
    ↑χ₄ ↑{ val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } * ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) }

case tail.tail.head

⊢ ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } =
    ↑χ₄ ↑{ val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } *
      ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) }

case tail.tail.tail.head

⊢ ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } =
    ↑χ₄ ↑{ val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } *
      ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) }

case tail.tail.tail.tail.head

⊢ ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } =
    ↑χ₄ ↑{ val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } *
      ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) }

case tail.tail.tail.tail.tail.head

⊢ ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } =
    ↑χ₄ ↑{ val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } *
      ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) }

case tail.tail.tail.tail.tail.tail.head

⊢ ↑χ₈'
      { val := 6,
        isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
    ↑χ₄
        ↑{ val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } *
      ↑χ₈
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) }

case tail.tail.tail.tail.tail.tail.tail.head

⊢ ↑χ₈'
      { val := 7,
        isLt :=
          (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
    ↑χ₄
        ↑{ val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } *
      ↑χ₈
        { val := 7,
          isLt :=
            (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) }
a : ZMod 8
⊢ ↑χ₈' a = ↑χ₄ ↑a * ↑χ₈ a
fin_cases a
no goals
case head

⊢ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } =
    ↑χ₄ ↑{ val := 0, isLt := (_ : 0 < 7 + 1) } * ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) }

case tail.head

⊢ ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } =
    ↑χ₄ ↑{ val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } * ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) }

case tail.tail.head

⊢ ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } =
    ↑χ₄ ↑{ val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } *
      ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) }

case tail.tail.tail.head

⊢ ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } =
    ↑χ₄ ↑{ val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } *
      ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) }

case tail.tail.tail.tail.head

⊢ ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } =
    ↑χ₄ ↑{ val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } *
      ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) }

case tail.tail.tail.tail.tail.head

⊢ ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } =
    ↑χ₄ ↑{ val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } *
      ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) }

case tail.tail.tail.tail.tail.tail.head

⊢ ↑χ₈'
      { val := 6,
        isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
    ↑χ₄
        ↑{ val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } *
      ↑χ₈
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) }

case tail.tail.tail.tail.tail.tail.tail.head

⊢ ↑χ₈'
      { val := 7,
        isLt :=
          (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
    ↑χ₄
        ↑{ val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } *
      ↑χ₈
        { val := 7,
          isLt :=
            (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) }
all_goals decide
no goals
case tail.tail.tail.tail.tail.tail.tail.head

⊢ ↑χ₈'
      { val := 7,
        isLt :=
          (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
    ↑χ₄
        ↑{ val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } *
      ↑χ₈
        { val := 7,
          isLt :=
            (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) }
decide