From 571b4bbd04cdeba9c51d0a0ea63c384cb9620f29 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 28 Sep 2024 17:41:54 +0200 Subject: [PATCH] Don't know what this line was doing over there --- src/Data/Real/Base.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Data/Real/Base.agda b/src/Data/Real/Base.agda index 3774427b6b..0da5045fc9 100644 --- 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) ∣