Fix deprecation for real

huynhtrankhanh · Nov 29, 2023 · c7fbf5e · c7fbf5e
1 parent 5c0d0b5
commit c7fbf5e
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/theories/FillInTheBlanks.v b/theories/FillInTheBlanks.v
@@ -349,9 +349,8 @@ Proof.
         lia. }
       assert (H1 : (2 * length withBlanks) / 2 = length withBlanks).
       { rewrite Nat.mul_comm. apply Nat.div_mul. easy. }
-      rewrite H. rewrite <- (Lcm0.divide_div_mul_exact _ _ _).
+      rewrite H. rewrite <- (Nat.Lcm0.divide_div_mul_exact _ _ _).
       * rewrite H1. rewrite subtractToCountNone. reflexivity.
-      * easy.
       * unfold possibleToFillBool in h.
         case_bool_decide; easy.
     + unfold possibleToFillBool in h.