Fix PredExp2

jonsterling · Oct 9, 2023 · 282e6d6 · 282e6d6
1 parent 291f09e
commit 282e6d6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Data/Nat/PredExp2.agda b/src/Data/Nat/PredExp2.agda
@@ -66,7 +66,7 @@ pred[2^suc[n]] n =
     pred (2 ^ n) + suc (pred (2 ^ n))
   ≡⟨ Eq.cong (pred (2 ^ n) +_) (suc-pred (2 ^ n) {{m^n≢0 2 n}}) ⟩
     pred (2 ^ n) + 2 ^ n
-  ≡˘⟨ +-∸-comm (2 ^ n) (2^n>0 n) ⟩
+  ≡˘⟨ +-∸-comm (2 ^ n) (m^n>0 2 n) ⟩
     pred (2 ^ n + 2 ^ n)
   ≡⟨ Eq.cong pred (lemma/2^suc n) ⟩
     pred (2 ^ suc n)