fix build failure caused by previous commit

mit-plv · May 3, 2022 · 994a547 · 994a547
1 parent c510bd8
commit 994a547
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Rupicola/Examples/Net/IPChecksum/Impl.v b/src/Rupicola/Examples/Net/IPChecksum/Impl.v
@@ -71,7 +71,7 @@ Section Properties.
          acc).
   Proof.
     intros.
-    rewrite div_up_eqn by lia.
+    rewrite Nat.div_up_eqn by lia.
     rewrite Nat2Z.inj_add.
     rewrite <- !fold_left_as_nd_ranged_for_all.
     rewrite (z_range_app 0 (Z.of_nat (n / 2)) (_ + _)) by lia.