search

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
288 stars 72 forks source link

unknown identifier 'not_iff_imp_false' error on Level 15 in the Inequality world #129

Open roozbeh-yz opened 1 year ago

roozbeh-yz commented 1 year ago

I can see that we have the not_iff_imp_false lemma in the left menu on Level 15 of the Inequality world. However, I get the unknown identifier error, when I try to use it. Should I import this lemma before using it? I have h2 : ¬b ≤ a, and I just want to execute rw not_iff_imp_false at h2.