chore: Restore a proof

dafny-lang · Dec 25, 2024 · afdec6b · afdec6b
1 parent 64374b3
commit afdec6b
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy
@@ -629,12 +629,15 @@ module Std.Arithmetic.DivMod {
     }
   }
 
-  lemma LemmaIndistinguishableQuotients(a: int, b: int, d: int)
+  lemma {:induction false} LemmaIndistinguishableQuotients(a: int, b: int, d: int)
     requires 0 < d
     requires 0 <= a - a % d <= b < a + d - a % d
     ensures a / d == b / d
   {
-    LemmaDivInductionAuto(d, a - b, ab => var u := ab + b; 0 <= u - u % d <= b < u + d - u % d ==> u / d == b / d);
+    var f := ab => var u := ab + b; 0 <= u - u % d <= b < u + d - u % d ==> u / d == b / d;
+    assert f(a - b) by {
+      LemmaDivInductionAuto(d, a - b, f);
+    }
   }
 
   lemma LemmaIndistinguishableQuotientsAuto()