diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 6d97cf87be48665165aaa88f44e5046cbd36949d..f4d7d6f3f22b1372479c4632594f1edf4d814824 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -73,7 +73,7 @@ Section mixin.
       { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } };
     mixin_cmra_maximum_idemp n (x : A) : ✓{n} x →
       { cx | cx ≼{n} x ∧ cx ⋅ cx ≡{n}≡ cx ∧ ∀ m (y : A), m ≤ n → y ≼{m} x → y ⋅ y ≡{m}≡ y → y ≼{m} cx } +
-      { ∀ m (y : A), m ≤ n → y ≼{m} x → y ⋅ y ≡{m}≡ y → False };
+      { ∀ y : A, y ≼{0} x → y ⋅ y ≡{0}≡ y → False };
   }.
 End mixin.
 
@@ -166,7 +166,7 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
   Lemma cmra_maximum_idemp n (x : A) : ✓{n} x →
     {cx | cx ≼{n} x ∧ cx ⋅ cx ≡{n}≡ cx ∧ ∀ m (y : A), m ≤ n → y ≼{m} x → y ⋅ y ≡{m}≡ y → y ≼{m} cx} +
-    { ∀ m (y : A), m ≤ n → y ≼{m} x → y ⋅ y ≡{m}≡ y → False }.
+    { ∀ y : A, y ≼{0} x → y ⋅ y ≡{0}≡ y → False }.
   Proof. apply (mixin_cmra_maximum_idemp _ (cmra_mixin A)). Qed.
 End cmra_mixin.
 
@@ -587,7 +587,7 @@ Section total_core.
   Proof.
     intros Hx.
     destruct (cmra_maximum_idemp n x Hx) as [?|H]; first done.
-    destruct (H n (core x))=>//.
+    destruct (H (core x))=>//.
     + exists x.
       by rewrite cmra_core_l.
     + by rewrite -cmra_core_dup.
@@ -1097,7 +1097,7 @@ Section discrete.
       destruct (maximum_idemp x) as [(cx & ? & ? & Hmax)|Hmax]=>//; [left|right].
       + exists cx; split_and! =>// m y ?.
         by apply Hmax.
-      + intros m y ??. by apply Hmax.
+      + done.
   Qed.
 
   Local Instance discrete_cmra_discrete :
@@ -1254,14 +1254,14 @@ Section prod.
       destruct (cmra_maximum_idemp n x.1) as [(c1 & Hx1 & ? & Hc1)|Hc1]=>//; first last.
       {
         right.
-        intros m y ? [??]%prod_includedN [??].
-        by apply (Hc1 m y.1).
+        intros y [??]%prod_includedN [??].
+        by apply (Hc1 y.1).
       }
       destruct (cmra_maximum_idemp n x.2) as [(c2 & Hx2 & ? & Hc2)|Hc2]=>//; first last.
       {
         right.
-        intros m y ? [??]%prod_includedN [??].
-        by apply (Hc2 m y.2).
+        intros y [??]%prod_includedN [??].
+        by apply (Hc2 y.2).
       }
       left.
       exists (c1, c2); split_and! =>//.
@@ -1563,9 +1563,11 @@ Section option.
           intros m ?? [->|(b & ? & -> & <-%(inj Some) & Hb)]%option_includedN.
           { by exists None. }
           intros ?%(inj Some).
-          destruct (Hc m b)=>//.
-          destruct Hb as [<- |?]=>//.
-          by exists b.
+          destruct (Hc b).
+          -- apply (cmra_includedN_le m); last lia.
+            destruct Hb as [<- |?]=>//.
+            by exists b.
+          -- by apply (dist_le m); last lia.
       + exists None; split_and! =>//.
         by exists None.
   Qed.
@@ -2051,19 +2053,18 @@ Proof.
           rewrite g_dist g_op Hc Hw assoc -g_op.
           by do 2 f_equiv.
       * right.
-        intros m z ? Hzy Hz.
-        specialize (Hcy m (g z)) as [w Hw]=>//.
-        {
-          destruct Hzy as [w Hw].
+        intros z Hzy Hz.
+        specialize (Hcy 0 (g z)) as [w Hw].
+        -- lia.
+        -- destruct Hzy as [w Hw].
           exists (g w).
           by rewrite -g_op -g_dist.
-        }
-        { by rewrite -g_op -g_dist. }
-        rewrite -g_opM_f symmetry_iff -gf_dist Hc in Hw.
-        inversion Hw.
+        -- by rewrite -g_op -g_dist.
+        -- rewrite -g_opM_f symmetry_iff -gf_dist Hc in Hw.
+          inversion Hw.
     + right.
-      intros m z ? Hzy Hz.
-      apply (Hcy m (g z))=>//.
+      intros z Hzy Hz.
+      apply (Hcy (g z))=>//.
       * destruct Hzy as [w ?].
         exists (g w).
         by rewrite -g_op -g_dist.
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 4686e5dabb227923b7f9b75d6fda0da92c1fa1c0..ac09b23f53370b3c2b140bed4f348e76a309c49d 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -274,9 +274,9 @@ Proof.
         intros ?%(inj Cinl).
         by apply Cinl_includedN, Hca.
       * right.
-        intros m ?? [?|[(a'&?&->&[= <-]&?)|(_&?&_&?&_)]]%csum_includedN=>//.
+        intros ? [?|[(a'&?&->&[= <-]&?)|(_&?&_&?&_)]]%csum_includedN=>//.
         intros ?%(inj Cinl).
-        by apply (Ha m a').
+        by apply (Ha a').
     + destruct (cmra_maximum_idemp n b) as [(cb & ? & ? & Hcb)|Hb]=>//.
       * left. exists (Cinr cb); split_and!.
         { by apply Cinr_includedN. }
@@ -285,9 +285,9 @@ Proof.
         intros ?%(inj Cinr).
         by apply Cinr_includedN, Hcb.
       * right.
-        intros m ?? [?|[(_&?&_&?&_)|(b'&?&->&[= <-]&?)]]%csum_includedN=>//.
+        intros ? [?|[(_&?&_&?&_)|(b'&?&->&[= <-]&?)]]%csum_includedN=>//.
         intros ?%(inj Cinr).
-        by apply (Hb m b').
+        by apply (Hb b').
 Qed.
 Canonical Structure csumR := Cmra (csum A B) csum_cmra_mixin.
 
diff --git a/iris/algebra/excl.v b/iris/algebra/excl.v
index 1bd54319638c86dd38d4841cd6b598b2ef9fb5d6..d2fc1a02d0b0e222fb5ef89c693318594a8e1e4d 100644
--- a/iris/algebra/excl.v
+++ b/iris/algebra/excl.v
@@ -90,7 +90,7 @@ Proof.
   - intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto.
   - intros n [?|]=>// _.
     right.
-    intros ?? _ [? He].
+    intros ? [? He].
     inversion He.
 Qed.
 Canonical Structure exclR := Cmra (excl A) excl_cmra_mixin.