small fix

marcinjangrzybowski · marcinjangrzybowski · commit 4f24bd7a57b4 · 2025-11-27T05:35:59.000+01:00
diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Rationals/Fast.agda b/Cubical/Algebra/OrderedCommRing/Instances/Rationals/Fast.agda
@@ -65,4 +65,4 @@ isOrderedCommRing (snd ℚOrderedCommRing) = isOrderedCommRingℚ
   isOrderedCommRingℚ .≤-<-trans       = isTrans≤<
   isOrderedCommRingℚ .·MonoR≤         = ≤-·o
   isOrderedCommRingℚ .·MonoR<         = <-·o
-  isOrderedCommRingℚ .0<1             = isRefl≤ 1
+  isOrderedCommRingℚ .0<1             = inj (_ , refl)
diff --git a/Cubical/HITs/CauchyReals/Lipschitz.agda b/Cubical/HITs/CauchyReals/Lipschitz.agda
@@ -1,6 +1,3 @@
--- {-# OPTIONS --safe --lossy-unification #-}
--- {-# OPTIONS --verbose intSolver:20 #-}
-
 module Cubical.HITs.CauchyReals.Lipschitz where
 
 open import Cubical.Foundations.Prelude
