Don't know what this line was doing over there

agda · Jan 21, 2025 · 84270bb · 84270bb
1 parent a14f5fd
commit 84270bb
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda
@@ -113,7 +113,8 @@ isCauchy (p *ₗ x) ε with p ≟ 0ℚ
 ... | no  p≢0 = proj₁ (isCauchy x (1/ ∣ p ∣ * ε)) , λ {m} {n} m≥N n≥N → begin-strict
   ∣ lookup (map (p *_) (sequence x)) m - lookup (map (p *_) (sequence x)) n ∣
     ≡⟨ cong₂ (λ a b → ∣ a - b ∣) (lookup-map m (p *_) (sequence x)) (lookup-map n (p *_) (sequence x)) ⟩
-  ∣ p * lookup (sequence x) m - p * lookup (sequence x) n ∣                   ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
+  ∣ p * lookup (sequence x) m - p * lookup (sequence x) n ∣
+    ≡⟨ cong (λ # → ∣ p * lookup (sequence x) m ℚ.+ # ∣) (neg-distribʳ-* p (lookup (sequence x) n)) ⟩
   ∣ p * lookup (sequence x) m ℚ.+ p * ℚ.- lookup (sequence x) n ∣
     ≡⟨ cong ∣_∣ (*-distribˡ-+ p (lookup (sequence x) m) (ℚ.- lookup (sequence x) n)) ⟨
   ∣ p * (lookup (sequence x) m - lookup (sequence x) n) ∣