theorem
proved
term proof
D_2_fails
show as:
view Lean formalization →
formal statement (Lean)
102theorem D_2_fails : ¬ is_fibonacci (2^2) := by native_decide
proof body
Term-mode proof.
103
104/-- D = 3 satisfies the Fibonacci constraint -/