Delete rewrite steps that do not fire (#2758)

Detected by a new warning for superfluous rewrites: agda/agda#7973

Author: andreasabel

src/Data/Integer/Properties.agda

@@ -1415,7 +1415,6 @@ private
         | [1+m]⊖[1+n]≡m⊖n (m ℕ.+ o ℕ.* suc m) (m ℕ.+ n ℕ.* suc m)
         | +-cancelˡ-⊖ m (o ℕ.* suc m) (n ℕ.* suc m)
         | ⊖-≥ n≤o
-        | +-comm (- (+ (m ℕ.+ n ℕ.* suc m))) (+ (m ℕ.+ o ℕ.* suc m))
         | ⊖-≥ (ℕ.*-mono-≤ n≤o (ℕ.≤-refl {x = suc m}))
         | ℕ.*-distribʳ-∸ (suc m) o n
         | +◃n≡+n (o ℕ.* suc m ∸ n ℕ.* suc m)

src/Induction/InfiniteDescent.agda

@@ -111,8 +111,8 @@ module _ (descent : Descent _<_ P) where
       h<P (suc n)           = g<P n
 
       Π[P∘h] : ∀ n →  P (h n)
-      Π[P∘h] zero rewrite g0≡z = py
-      Π[P∘h] (suc n)           = Π[P∘g] n
+      Π[P∘h] zero    = py
+      Π[P∘h] (suc n) = Π[P∘g] n
 
   descent∧wf⇒infiniteDescent : WellFounded _<_ → InfiniteDescent _<_ P
   descent∧wf⇒infiniteDescent wf = descent∧acc⇒infiniteDescentFrom (wf _)