diff --git a/actris/channel/proto.v b/actris/channel/proto.v
index 531c87151c572faeaa87200f05f0e159520f0ab3..bb3e9c6b36e031b8e4d27b458ca69e6eac629057 100644
--- a/actris/channel/proto.v
+++ b/actris/channel/proto.v
@@ -526,7 +526,7 @@ Section proto.
     destruct (iProto_case p1) as [->|(a&m&->)].
     { by rewrite !left_id. }
     rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
-    f_contractive. apply IH; eauto using dist_le with lia.
+    f_contractive. apply IH; eauto using dist_lt.
   Qed.
   Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
   Proof. apply (ne_proper_2 _). Qed.
diff --git a/actris/channel/proto_model.v b/actris/channel/proto_model.v
index 9f73151a05674aa327422b9db763bc81672cf389..ed172910c23888a325a4ddffdf0993d5ef588bee 100644
--- a/actris/channel/proto_model.v
+++ b/actris/channel/proto_model.v
@@ -213,7 +213,7 @@ Proof.
   induction (lt_wf n) as [n _ IH]=>
     PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
   etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
-  apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
+  apply proto_map_aux_contractive; constructor=> n' ?. symmetry. by apply: IH.
 Qed.
 Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
@@ -241,7 +241,7 @@ Proof.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=.
   apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
-  apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia.
+  apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_lt.
 Qed.
 Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
diff --git a/actris/utils/cofe_solver_2.v b/actris/utils/cofe_solver_2.v
index 7a2425ba1241530b55ba7d0572cb276d271f7728..43a65db72120c57f19123c4cc5bea80371bdbd31 100644
--- a/actris/utils/cofe_solver_2.v
+++ b/actris/utils/cofe_solver_2.v
@@ -14,8 +14,8 @@ Global Existing Instance solution_2_cofe.
 Section cofe_solver_2.
   Context (F : ofe → oFunctor).
   Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
-  Context `{Fcofe : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
-  Context `{Finh : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
+  Context `{Fcofe : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
+  Context `{Finh : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
   Notation map := (oFunctor_map (F _)).
 
   Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=
diff --git a/coq-actris.opam b/coq-actris.opam
index 05d599400f55254149213226713b4ae7e1ac0d99..95134023b2ee879ea25321eb013779ee183fb717 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2025-02-27.1.c773500a") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
 ]
 
 build: ["./make-package" "actris" "-j%{jobs}%"]
diff --git a/multris/channel/proto.v b/multris/channel/proto.v
index 3dc14415d891f23a7ad57262393b7af79bd65fc0..4b8df7aaf76fdc4e7861e73867531e28df08be70 100644
--- a/multris/channel/proto.v
+++ b/multris/channel/proto.v
@@ -389,7 +389,7 @@ Section proto.
     destruct (iProto_case p1) as [->|(a&i&m&->)].
     { by rewrite !left_id. }
     rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
-    f_contractive. apply IH; eauto using dist_le with lia.
+    f_contractive. apply IH; eauto using dist_lt.
   Qed.
   Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
   Proof. apply (ne_proper_2 _). Qed.
diff --git a/multris/channel/proto_model.v b/multris/channel/proto_model.v
index 77a71e10ee887deb88e95e4da68984959a0514e5..25fb5963af5be260e090cf91e254922404799e0e 100644
--- a/multris/channel/proto_model.v
+++ b/multris/channel/proto_model.v
@@ -214,7 +214,7 @@ Proof.
   induction (lt_wf n) as [n _ IH]=>
     PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
   etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
-  apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
+  apply proto_map_aux_contractive. constructor=> n' ?. symmetry. by apply: IH.
 Qed.
 Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
@@ -242,7 +242,7 @@ Proof.
   destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
   rewrite !proto_map_message /=.
   apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
-  apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia.
+  apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_lt.
 Qed.
 Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
diff --git a/multris/utils/cofe_solver_2.v b/multris/utils/cofe_solver_2.v
index 7a2425ba1241530b55ba7d0572cb276d271f7728..43a65db72120c57f19123c4cc5bea80371bdbd31 100644
--- a/multris/utils/cofe_solver_2.v
+++ b/multris/utils/cofe_solver_2.v
@@ -14,8 +14,8 @@ Global Existing Instance solution_2_cofe.
 Section cofe_solver_2.
   Context (F : ofe → oFunctor).
   Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
-  Context `{Fcofe : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
-  Context `{Finh : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
+  Context `{Fcofe : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
+  Context `{Finh : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
   Notation map := (oFunctor_map (F _)).
 
   Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=