diff --git a/refinedc.opam b/refinedc.opam
index 127f67b48d205c15a9fac932c3960baf6c646a4f..fdb503c33729ac27259fdb26f417128bef59c144 100644
--- a/refinedc.opam
+++ b/refinedc.opam
@@ -16,7 +16,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
 
 depends: [
-  "coq" { (>= "8.11.0" & < "8.12~") }
+  "coq" { (>= "8.12.0" & < "8.13~") }
   "coq-iris" { (= "dev.2020-10-01.3.8f6c063a") | (= "dev") }
   "dune" {>= "2.7.0"}
   "cerberus" {= "~dev"}
diff --git a/theories/lang/base.v b/theories/lang/base.v
index 0b380fdaa35fe2f227faa11b2ab4568228f50d41..b285da5cc5e159c623162688b32d726f767981ee 100644
--- a/theories/lang/base.v
+++ b/theories/lang/base.v
@@ -379,7 +379,7 @@ Definition keep_factor2 (n : nat) (def : nat) : nat :=
 
 Lemma Pos_pow_add_r a b c:
   (a ^ (b + c) = a ^ b * a ^ c)%positive.
-Proof. zify. rewrite !Pos2Z.inj_pow Pos2Z.inj_add Z.pow_add_r; lia. Qed.
+Proof. zify. rewrite Z.pow_add_r; lia. Qed.
 
 Lemma Pos_factor2_mult_xI a b:
   Pos_factor2 (a~1 * b) = Pos_factor2 b.
diff --git a/theories/lithium/simpl_instances.v b/theories/lithium/simpl_instances.v
index 308a2eed525c2497deb42bb6cb5ce9f9ceb085c3..b41bbd69f0663c3f7f91a6d5e5a95c88f10b5658 100644
--- a/theories/lithium/simpl_instances.v
+++ b/theories/lithium/simpl_instances.v
@@ -93,7 +93,6 @@ Proof.
   unfold CanSolve in *. rewrite /Z.divide. split.
   - move => HT [x Hx]. apply: (HT (Z.to_nat x)).
     rewrite -Z2Nat.inj_mul; try lia.
-    apply (Z.mul_nonneg_cancel_r _ a); lia.
   - move => HT n ?. apply HT. eexists n. lia.
 Qed.