diff --git a/Game/MyNat/LE.lean b/Game/MyNat/LE.lean index 1917e33..c741c50 100644 --- a/Game/MyNat/LE.lean +++ b/Game/MyNat/LE.lean @@ -1,5 +1,5 @@ import Game.MyNat.Multiplication -import Mathlib.Tactic +--import Mathlib.Tactic namespace MyNat