Representing every amount above three with two and five

Given debt N: If N is even and $N \ge 4$ , then use $\frac{N}{2}$ two dollar bills. If N is odd, use one 5 dollar bill and $\frac{N-5}{2}$ two dollar bills. This works for all $N \ge 4$

Source: InternLM Lean-Workbook, record lean_workbook_plus_65242 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.