1. State and prove Fel's conjecture in Lean.