I find it incredibly impressive you did this in 15 minutes! You should really help out in formalizing math (completely serious).

Personally in the past I tried a few times to formalize some statements and sometimes I found that the mathlib libraries were pretty lacking in these more open-ended problems (I wanted to reason about lists and stuff). But it seems that I am just very bad at formalization lol.