Move instances to testing file, delete leftover theo

Signed-off-by: Adrian Palacios <accorell@amazon.com>

cedar-lean/Cedar/Spec/Ext/Datetime.lean

@@ -136,17 +136,6 @@ instance Duration.decLe (d₁ d₂ : Duration) : Decidable (d₁ ≤ d₂) :=
 instance : Coe Int64 Duration where
   coe i := Duration.mk i
 
--- Note: The instances below are only used for tests.
--- We might redefine them if they are need for something else.
-instance : OfNat Duration n where
-  ofNat := ⟨Int64.ofNat n⟩
-
-instance : ToString Duration where
-  toString d := toString d.val
-
-instance : Neg Duration where
-  neg d := ⟨-d.val⟩
-
 def MILLISECONDS_PER_SECOND: Int := 1000
 def MILLISECONDS_PER_MINUTE: Int := 60000
 def MILLISECONDS_PER_HOUR: Int := 360000

cedar-lean/UnitTest/Datetime.lean

@@ -89,7 +89,16 @@ def testsForInvalidDatetimeStrings :=
     testInvalidDatetime "2016-12-31T00:00:00+9999" "invalid offset range",
   ]
 
-theorem testDuration16 : toString ((Duration.parse "0d0h0m0s0ms").get!) = "0" := by native_decide
+-- Note: The instances below are only used for tests.
+-- We might redefine them if they are need for something else.
+instance : OfNat Duration n where
+  ofNat := ⟨Int64.ofNat n⟩
+
+instance : ToString Duration where
+  toString d := toString d.val
+
+instance : Neg Duration where
+  neg d := ⟨-d.val⟩
 
 private def testValidDuration (str : String) (rep : Int) : TestCase IO :=
   test str ⟨λ _ => checkEq (Duration.parse str) (duration? rep)⟩