Fix proof

dafny-lang · Oct 10, 2023 · 1ed937b · 1ed937b
1 parent 4288684
commit 1ed937b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Math/Analysis/Limits.dfy b/src/Math/Analysis/Limits.dfy
@@ -150,7 +150,7 @@ module Limits {
           var s2 := sequence2(n);
           calc {
             Reals.Dist(productSequence(n), productLimit);
-          == { assert productSequence(n) == s1 * s2; }
+          == { assert productSequence(n) == sequence1(n) * sequence2(n) == s1 * s2; }
             Reals.Dist(s1 * s2, limit1 * limit2);
           < { LimitIsMultiplicativeSuffixHelper(s1, limit1, s2, limit2, bound1, epsilon); }
             epsilon;