feat: LT for Timestamp and Duration (#8422)

This PR adds `LT` and `Decidable` `LT` instances for
`Std.Time.Timestamp` and `Std.Time.Duration`.

Author: hargoniX

src/Std/Time/DateTime/Timestamp.lean

@@ -34,6 +34,12 @@ instance : LE Timestamp where
 instance { x y : Timestamp } : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.val ≤ y.val))
 
+instance : LT Timestamp where
+  lt x y := x.val < y.val
+
+instance { x y : Timestamp } : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
 instance : OfNat Timestamp n where
   ofNat := ⟨OfNat.ofNat n⟩
 

src/Std/Time/Duration.lean

@@ -156,6 +156,12 @@ instance : LE Duration where
 instance {x y : Duration} : Decidable (x ≤ y) :=
   inferInstanceAs (Decidable (x.toNanoseconds ≤ y.toNanoseconds))
 
+instance : LT Duration where
+  lt d1 d2 := d1.toNanoseconds < d2.toNanoseconds
+
+instance {x y : Duration} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.toNanoseconds < y.toNanoseconds))
+
 /--
 Converts a `Duration` to a `Minute.Offset`
 -/