diff --git a/theories/FillInTheBlanks.v b/theories/FillInTheBlanks.v
index 1035327..75d5a61 100644
--- 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.