diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f73d6593ab..17f64a41d5 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -208,6 +208,14 @@
 - in `realsum.v`:
   + lemma `__admitted__psumB` proved and renamed to `psumB`
 
+- in `realsum.v`:
+  + lemmas `interchange_sup`, `interchange_psum` are no longer
+    deprecated
+- in `distr.v`:
+  + lemmas `dlet_dlet`, `dmargin_dlet`, `dlet_dmargin`, `dfst_dswap`,
+    `dsnd_dswap`, `dsndE`, `pr_dlet` are no longer deprecated
+
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
diff --git a/experimental_reals/distr.v b/experimental_reals/distr.v
index c9baefbf2c..77b863797b 100644
--- a/experimental_reals/distr.v
+++ b/experimental_reals/distr.v
@@ -505,7 +505,7 @@ End BindTheory.
 Section DLetDLet.
 Context {T U V : choiceType} (f1 : T -> distr U) (f2 : U -> distr V).
 
-Lemma __deprecated__dlet_dlet (mu : {distr T / R}) :
+Lemma dlet_dlet (mu : {distr T / R}) :
      \dlet_(x <- \dlet_(y <- mu) f1 y) f2 x
   =1 \dlet_(y <- mu) (\dlet_(x <- f1 y) f2 x).
 Proof.
@@ -513,7 +513,7 @@ move=> z; unlock dlet => /=; rewrite /mlet /=.
 pose S y x := mu x * (f1 x y * f2 y z).
 rewrite (eq_psum (F2 := fun y => PosSum.psum (S^~ y))) => [x|].
   by rewrite -psumZ //; apply/eq_psum => y /=.
-rewrite __admitted__interchange_psum.
+rewrite interchange_psum.
 + by move=> x; apply/summableZ/summable_mlet.
 + rewrite {}/S; apply/(le_summable (F2 := mu)) => //.
   move=> x; rewrite ge0_psum /= psumZ ?ler_piMr //.
@@ -522,8 +522,12 @@ rewrite __admitted__interchange_psum.
 apply/eq_psum=> y /=; rewrite -psumZr //.
 by apply/eq_psum=> x /=; rewrite {}/S mulrA.
 Qed.
+
 End DLetDLet.
 
+#[deprecated(since="1.17.0", note="use `dlet_dlet` instead")]
+Notation __deprecated__dlet_dlet := dlet_dlet (only parsing).
+
 (* -------------------------------------------------------------------- *)
 Section DLetAlg.
 Context {T U : choiceType} (mu mu1 mu2 : {distr T / R}).
@@ -719,16 +723,16 @@ rewrite dmarginE dletE; apply/eq_psum => x //=.
 by rewrite mulrC dunit1E.
 Qed.
 
-Lemma __deprecated__dlet_dmargin (mu : {distr T / R}) (f : T -> U) (g : U -> {distr V / R}):
+Lemma dlet_dmargin (mu : {distr T / R}) (f : T -> U) (g : U -> {distr V / R}):
   \dlet_(u <- dmargin f mu) g u =1 \dlet_(t <- mu) (g (f t)).
 Proof.
-move=> x; rewrite __deprecated__dlet_dlet; apply: eq_in_dlet=> //.
+move=> x; rewrite dlet_dlet; apply: eq_in_dlet=> //.
 by move=> y _ z; rewrite dlet_unit.
 Qed.
 
-Lemma __deprecated__dmargin_dlet (mu : {distr T / R}) (f : U -> V) (g : T -> {distr U / R}):
+Lemma dmargin_dlet (mu : {distr T / R}) (f : U -> V) (g : T -> {distr U / R}):
   dmargin f (\dlet_(t <- mu) g t) =1 \dlet_(t <- mu) (dmargin f (g t)).
-Proof. by apply/__deprecated__dlet_dlet. Qed.
+Proof. by apply/dlet_dlet. Qed.
 
 Lemma dmargin_dunit (t : T) (f : T -> U):
   dmargin f (dunit t) =1 dunit (f t) :> {distr U / R}.
@@ -736,15 +740,10 @@ Proof. by apply/dlet_unit. Qed.
 End MarginalsTh.
 End Std.
 
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="relies on admitted, use __deprecated__dlet_dlet explicitly if you really want to use this lemma")]
-Notation dlet_dlet := __deprecated__dlet_dlet.
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="relies on admitted, use __deprecated__dmargin_dlet explicitly if you really want to use this lemma")]
-Notation dmargin_dlet := __deprecated__dmargin_dlet.
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="relies on admitted, use __deprecated__dlet_dmargin explicitly if you really want to use this lemma")]
-Notation dlet_dmargin := __deprecated__dlet_dmargin.
+#[deprecated(since="1.17.0", note="use `dmargin_dlet` instead")]
+Notation __deprecated__dmargin_dlet := dmargin_dlet (only parsing).
+#[deprecated(since="1.17.0", note="use `dlet_dmargin` instead")]
+Notation __deprecated__dlet_dmargin := dlet_dmargin (only parsing).
 
 Notation dfst mu := (dmargin fst mu).
 Notation dsnd mu := (dmargin snd mu).
@@ -787,25 +786,23 @@ Proof.
 by move=> h; apply/dinsuppP; rewrite dswapE; apply/dinsuppPn.
 Qed.
 
-Lemma __deprecated__dfst_dswap : dfst (dswap mu) =1 dsnd mu.
+Lemma dfst_dswap : dfst (dswap mu) =1 dsnd mu.
 Proof.
-move=> z; rewrite __deprecated__dlet_dlet; apply/eq_in_dlet => // -[x y].
+move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
 by move=> _ t /=; rewrite dlet_unit /=.
 Qed.
 
-Lemma __deprecated__dsnd_dswap : dsnd (dswap mu) =1 dfst mu.
+Lemma dsnd_dswap : dsnd (dswap mu) =1 dfst mu.
 Proof.
-move=> z; rewrite __deprecated__dlet_dlet; apply/eq_in_dlet => // -[x y].
+move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
 by move=> _ t /=; rewrite dlet_unit /=.
 Qed.
 End DSwapTheory.
 
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="relies on admitted, use __deprecated__dfst_dswap explicitly if you really want to use this lemma")]
-Notation dfst_dswap := __deprecated__dfst_dswap.
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="relies on admitted, use __deprecated__dsnd_dswap explicitly if you really want to use this lemma")]
-Notation dsnd_dswap := __deprecated__dsnd_dswap.
+#[deprecated(since="1.17.0", note="use `dfst_dswap` instead")]
+Notation __deprecated__dfst_dswap := dfst_dswap (only parsing).
+#[deprecated(since="1.17.0", note="use `dsnd_dswap` instead")]
+Notation __deprecated__dsnd_dswap := dsnd_dswap (only parsing).
 
 (* -------------------------------------------------------------------- *)
 Section DFst.
@@ -836,9 +833,9 @@ End DFst.
 Section DSnd.
 Context {R : realType} {T U : choiceType}.
 
-Lemma __deprecated__dsndE (mu : {distr (T * U) / R}) y :
+Lemma dsndE (mu : {distr (T * U) / R}) y :
   dsnd mu y = PosSum.psum (fun x => mu (x, y)).
-Proof. by rewrite -__deprecated__dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.
+Proof. by rewrite -dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.
 
 Lemma summable_snd (mu : {distr (T * U) / R}) y :
   summable (fun x => mu (x, y)).
@@ -848,9 +845,8 @@ by move=> x /=; rewrite dswapE.
 Qed.
 End DSnd.
 
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="relies on admitted, use __deprecated__dsndE explicitly if you really want to use this lemma")]
-Notation dsndE := __deprecated__dsndE.
+#[deprecated(since="1.17.0", note="use `dsndE` instead")]
+Notation __deprecated__dsndE := dsndE (only parsing).
 
 (* -------------------------------------------------------------------- *)
 Section PrCoreTheory.
@@ -957,7 +953,7 @@ Context {R : realType} {T U : choiceType} {I : eqType}.
 
 Implicit Types (mu : {distr T / R}) (A B E : pred T).
 
-Lemma __deprecated__pr_dlet E f (mu : {distr U / R}) :
+Lemma pr_dlet E f (mu : {distr U / R}) :
   \P_[dlet f mu] E = \E_[mu] (fun x => \P_[f x] E).
 Proof.
 rewrite /esp -psum_sum => [x|]; first by rewrite mulr_ge0 ?ge0_pr.
@@ -965,7 +961,7 @@ rewrite /pr; unlock dlet => /=; rewrite /mlet /=.
 pose F x y := (E x)%:R * (mu y * f y x).
 transitivity (PosSum.psum (fun x => PosSum.psum (fun y => F x y))); rewrite {}/F.
   by apply/eq_psum => x; rewrite -psumZ ?ler0n.
-rewrite __admitted__interchange_psum /=; last first.
+rewrite interchange_psum /=; last first.
   apply/eq_psum=> y /=; rewrite mulrC -psumZ //.
   by apply/eq_psum=> x /=; rewrite mulrCA.
 + have := summable_pr E (dlet f mu); apply/eq_summable.
@@ -976,7 +972,7 @@ Qed.
 Lemma pr_dmargin E f (mu : {distr U / R}) :
   \P_[dmargin f mu] E = \P_[mu] [pred x | f x \in E].
 Proof.
-by rewrite /dmargin __deprecated__pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit.
+by rewrite /dmargin pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit.
 Qed.
 
 Lemma eq0_pr A mu :
@@ -1208,9 +1204,9 @@ Lemma __admitted__exp_dlet mu (nu : T -> {distr U / R}) F :
 Proof using Type*. Admitted.
 End PrTheory.
 
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="relies on admitted, use __deprecated__pr_dlet explicitly if you really want to use this lemma")]
-Notation pr_dlet := __deprecated__pr_dlet.
+#[deprecated(since="1.17.0", note="use `pr_dlet` instead")]
+Notation __deprecated__pr_dlet := pr_dlet (only parsing).
+
 #[deprecated(since="mathcomp-analysis 0.6.2",
   note="lacks proof, use __admitted__exp_split explicitly if you really want to use this lemma")]
 Notation exp_split := __admitted__exp_split.
diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v
index ad5766cdcc..d56fbe32bb 100644
--- a/experimental_reals/realsum.v
+++ b/experimental_reals/realsum.v
@@ -680,10 +680,8 @@ Qed.
 (* -------------------------------------------------------------------- *)
 Section StdSum.
 Context {R : realType} (T : choiceType) (I : Type).
+Implicit Type f g S : T -> R.
 
-Implicit Type S : T -> R.
-
-(* -------------------------------------------------------------------- *)
 Lemma psum0 : PosSum.psum (fun _ : T => 0) = 0 :> R.
 Proof.
 rewrite /PosSum.psum asboolT; first by apply/summable0.
@@ -694,12 +692,10 @@ rewrite predeqE => x; split.
 by move=> ->; exists fset0; rewrite big_fset0.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma psum_eq0 (f : T -> R) : (forall x, f x = 0) -> PosSum.psum f = 0.
+Lemma psum_eq0 f : (forall x, f x = 0) -> PosSum.psum f = 0.
 Proof. by move=> eq; rewrite (eq_psum eq) psum0. Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma eq0_psum (f : T -> R) :
+Lemma eq0_psum f :
   summable f -> PosSum.psum f = 0 -> (forall x : T, f x = 0).
 Proof.
 move=> sm psum_eq0 x; apply/eqP; rewrite -normr_eq0.
@@ -708,14 +704,12 @@ apply/(le_trans _ (gerfinseq_psum (r := [:: x]) _ sm)) => //.
 by rewrite big_seq1.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma neq0_psum (f : T -> R) : PosSum.psum f <> 0 -> exists x : T, f x <> 0.
+Lemma neq0_psum f : PosSum.psum f <> 0 -> exists x : T, f x <> 0.
 Proof.
 by move=> nz_psum; apply/existsp_asboolPn/asboolPn => /psum_eq0.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma psum_abs (S : T -> R) : PosSum.psum \`|S| = PosSum.psum S.
+Lemma psum_abs S : PosSum.psum \`|S| = PosSum.psum S.
 Proof.
 rewrite /PosSum.psum; do 2! case: ifPn => //; first last.
 + by move/asboolP/summable_abs/asboolP=> ->.
@@ -727,31 +721,26 @@ case=> J ->; exists J.
 by under [in RHS]eq_bigr do rewrite normr_id.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma eq_psum_abs (S1 S2 : T -> R) :
-  \`|S1| =1 \`|S2| -> PosSum.psum S1 = PosSum.psum S2.
+Lemma eq_psum_abs S1 S2 : \`|S1| =1 \`|S2| -> PosSum.psum S1 = PosSum.psum S2.
 Proof.
 by move=> eqS; rewrite -[LHS]psum_abs -[RHS]psum_abs; apply/eq_psum.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma le_psum_abs (S1 S2 : T -> R) :
-  (forall x, `|S1 x| <= `|S2 x|) -> summable S2 -> PosSum.psum S1 <= PosSum.psum S2.
+Lemma le_psum_abs S1 S2 : (forall x, `|S1 x| <= `|S2 x|) -> summable S2 ->
+  PosSum.psum S1 <= PosSum.psum S2.
 Proof.
 move=> leS smS2; rewrite -[X in X<=_]psum_abs -[X in _<=X]psum_abs.
 by apply/le_psum/summable_abs => // x; rewrite normr_ge0 leS.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma le_psum_condl (S : T -> R) (P : pred T) :
+Lemma le_psum_condl S (P : pred T) :
   summable S -> PosSum.psum (fun x => (P x)%:R * S x) <= PosSum.psum S.
 Proof.
 move=> smS; apply/le_psum_abs=> // x; rewrite normrM.
 by apply/ler_piMl => //; rewrite normr_nat lern1 leq_b1.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma le_psum_condr (S : T -> R) (P : pred T) :
+Lemma le_psum_condr S (P : pred T) :
   summable S -> PosSum.psum (fun x => S x * (P x)%:R) <= PosSum.psum S.
 Proof.
 move=> smS; apply/(le_trans _ (le_psum_condl P smS)).
@@ -759,8 +748,7 @@ rewrite le_eqVlt -(rwP orP); left; apply/eqP/eq_psum.
 by move=> x /=; rewrite mulrC.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma psumN (S : T -> R) : PosSum.psum (- S) = PosSum.psum S.
+Lemma psumN S : PosSum.psum (- S) = PosSum.psum S.
 Proof.
 case/boolP: `[< summable S >] => h; last first.
   by rewrite !psum_out ?oppr0 //; apply/asboolPn; rewrite ?summablebN.
@@ -768,7 +756,6 @@ rewrite /PosSum.psum summablebN h; apply/eq_ppsum=> J /=.
 by apply/eq_bigr=> j _; rewrite normrN.
 Qed.
 
-(* -------------------------------------------------------------------- *)
 Lemma psumD S1 S2 :
     (forall x, 0 <= S1 x) -> (forall x, 0 <= S2 x)
   -> summable S1 -> summable S2
@@ -796,30 +783,18 @@ rewrite /D big_split /=; apply/lerD; apply/big_fset_subset=> //.
 + by apply/fsubsetP/fsubsetUl. + by apply/fsubsetP/fsubsetUr.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-
-Lemma psumB S1 S2 :
-    (forall x, 0 <= S2 x <= S1 x) -> summable S1
-  -> PosSum.psum (S1 \- S2) = (PosSum.psum S1 - PosSum.psum S2).
-Proof.
-move=> S2S1 sumS1; apply: EFin_inj; rewrite EFinB.
-have sumS2 : summable S2 by exact: le_summable sumS1.
-rewrite -(@esum_psum _ _ S1)//.
-  by move=> t; have /andP[S20] := S2S1 t; exact: le_trans.
-rewrite -(@esum_psum _ _ S2)//.
-  by move=> t; have /andP[] := S2S1 t.
-rewrite -esumB//.
-- exact/esum_summableP.
-- exact/esum_summableP.
-- by move=> t _; rewrite lee_fin; have /andP[S20] := S2S1 t; exact: le_trans.
-- by move=> t _; rewrite lee_fin; have /andP[] := S2S1 t.
-rewrite -esum_psum.
-- by move=> t; rewrite subr_ge0; have /andP[] := S2S1 t.
-  by apply: summableD => //; exact: summableN.
-by rewrite {1}/esum; congr (_ - _)%E; rewrite ge0_esum.
+Lemma psumB f g : (forall x, 0 <= g x <= f x) -> summable f ->
+  PosSum.psum (f \- g) = PosSum.psum f - PosSum.psum g.
+Proof.
+move=> gf0 sumf.
+have g0 x : 0 <= g x by have /andP[] := gf0 x.
+have gf x : g x <= f x by have /andP[] := gf0 x.
+rewrite -[in RHS](subrK g f) [in RHS]psumD ?addrK//.
+- by move=> x; rewrite subr_ge0.
+- by apply: le_summable sumf => x; rewrite subr_ge0 gf lerBlDr lerDl g0.
+- exact: le_summable sumf.
 Qed.
 
-(* -------------------------------------------------------------------- *)
 Lemma psumZ S c : 0 <= c -> PosSum.psum (c \*o S) = c * PosSum.psum S.
 Proof.
 rewrite le_eqVlt => /orP[/eqP<-|gt0_c].
@@ -843,15 +818,12 @@ rewrite mulr_sumr; apply/(le_trans _ (gerfin_psum J _))=> //.
 by apply/ler_sum=> /= j _; rewrite normrM (gtr0_norm gt0_c).
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma psumZr S c :
-  0 <= c -> PosSum.psum (c \o* S) = PosSum.psum S * c.
+Lemma psumZr S c : 0 <= c -> PosSum.psum (c \o* S) = PosSum.psum S * c.
 Proof.
 move=> ge0_c; rewrite [RHS]mulrC -psumZ //.
 by apply/eq_psum => x /=; rewrite mulrC.
 Qed.
 
-(* -------------------------------------------------------------------- *)
 Lemma psum_bigop (F : I -> T -> R) P r :
     (forall i x, 0 <= F i x) -> (forall i, summable (F i)) ->
   \sum_(i <- r | P i) PosSum.psum (F i) =
@@ -866,10 +838,9 @@ rewrite -psumD //; first by move=> x; apply/sumr_ge0.
 by apply/eq_psum=> x /=; rewrite big_cons Pi.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma psumID S (P : pred T) :
-  summable S -> PosSum.psum S =
-    PosSum.psum (fun x => (P x)%:R * S x) + PosSum.psum (fun x => (~~P x)%:R * S x).
+Lemma psumID S (P : pred T) : summable S ->
+  PosSum.psum S =
+  PosSum.psum (fun x => (P x)%:R * S x) + PosSum.psum (fun x => (~~P x)%:R * S x).
 Proof.
 have h x: `|S x| = (P x)%:R * `|S x| + (~~P x)%:R * `|S x|.
   by case: (P x); rewrite !Monoid.simpm.
@@ -882,10 +853,8 @@ congr (_ + _); apply/eq_psum_abs=> x /=.
   by rewrite !normrM normr_nat normr_id.
 Qed.
 
-(* -------------------------------------------------------------------- *)
-Lemma psum_finseq S (r : seq.seq T) :
-    uniq r -> {subset [pred x | S x != 0] <= r}
-  -> PosSum.psum S = \sum_(x <- r) `|S x|.
+Lemma psum_finseq S (r : seq T) : uniq r -> {subset [pred x | S x != 0] <= r} ->
+  PosSum.psum S = \sum_(x <- r) `|S x|.
 Proof.
 move=> eq_r ler; set s := RHS; have h J: uniq J -> \sum_(x <- J) `|S x| <= s.
   move=> uqJ; rewrite (bigID (ssrbool.mem r)) /= addrC big1.
@@ -900,10 +869,11 @@ move=> eq_r ler; set s := RHS; have h J: uniq J -> \sum_(x <- J) `|S x| <= s.
 case/summable_of_bd: h => smS le_psum; apply/eqP.
 by rewrite eq_le le_psum /=; apply/gerfinseq_psum.
 Qed.
+
 End StdSum.
 
 #[deprecated(since="1.17.0", note="use `psumB` instead")]
-Notation __admitted__psumB :=psumB.
+Notation __admitted__psumB := psumB (only parsing).
 
 (* -------------------------------------------------------------------- *)
 Section PSumReindex.
@@ -1091,37 +1061,112 @@ Qed.
 
 End PSumPair.
 
+(* -------------------------------------------------------------------- *)
+Section PSumPairSummable.
+Context {R : realType} {T U : choiceType}.
+
+Local Lemma summable_pair_from_rows_psum (S : T -> U -> R) :
+    (forall x, summable (S x)) ->
+    summable (fun x => PosSum.psum (S x)) ->
+  summable (fun xy => S xy.1 xy.2).
+Proof.
+move=> sumS sum_psumS.
+exists (PosSum.psum (PosSum.psum \o S)) => J.
+rewrite (big_fset_seq (fun xy => `|S xy.1 xy.2|))/=.
+rewrite (partition_big_imfset _ fst J (fun xy => `|S xy.1 xy.2|))/=.
+pose X := [fset xy.1 | xy in J]%fset.
+have := gerfin_psum X sum_psumS.
+rewrite (big_fset_seq (fun x => `|PosSum.psum (S x)|))/=.
+apply: le_trans; apply: ler_sum => x _.
+rewrite ger0_norm ?ge0_psum//.
+pose F := [fset xy in J | xy.1 == x]%fset.
+rewrite [leLHS](_ :  _ = \sum_(xy <- F) `|S x xy.2|).
+  by rewrite /F big_fset /=; apply: eq_bigr => xy /eqP ->.
+rewrite -(big_map snd predT (fun y => `|S x y|)).
+apply: gerfinseq_psum => //.
+rewrite map_inj_in_uniq; last exact: uniq_fset_keys.
+move=> [x1 y1] [x2 y2] /[!in_fset] /= /[!inE] /=.
+by move=> /andP[_ /eqP ->] /andP[_ /eqP /= ->] ->.
+Qed.
+
+End PSumPairSummable.
+
 (* -------------------------------------------------------------------- *)
 (* FIXME: MOVE ME                                                       *)
 Section SupInterchange.
 Context {R : realType} {T U : Type}.
+Variable S : T -> U -> R.
+
+Local Open Scope classical_set_scope.
+
+Let row x := range (S x).
+Let col y := range (S ^~ y).
+Let rows := range (sup \o row).
+Let cols := range (sup \o col).
+
+Lemma interchange_sup : (forall x, has_sup (row x)) -> has_sup rows ->
+  sup rows = sup cols.
+Proof.
+move=> row_sup rows_sup.
+have col_nonempty y : col y !=set0.
+  by case: rows_sup => + _ => -[_ [x _ _]]; eexists; exact/imageT.
+have col_bound y : ubound (col y) (sup rows).
+  move=> _ [x _ <-]; apply: le_trans.
+  - have /sup_upper_bound := row_sup x.
+    by apply; exact/imageT.
+  - have /sup_upper_bound := rows_sup.
+    by apply; exact/imageT.
+have col_le_rows y : sup (col y) <= sup rows.
+  by apply: ge_sup; [exact: col_nonempty|exact: col_bound].
+have cols_sup : has_sup cols.
+  split.
+  - case: rows_sup => + _ => -[_ [x _ _]].
+    case: (row_sup x) => + _ => -[_ [y _ _]].
+    by eexists; exact/imageT.
+  - by exists (sup rows) => _ [y _ <-]; exact: col_le_rows.
+apply/eqP; rewrite eq_le; apply/andP; split.
+- apply: ge_sup; first by case: rows_sup.
+  move=> _ [x _ <-].
+  apply: ge_sup; first by have [] := row_sup x.
+  move=> ? [y _ <-]; apply: le_trans.
+    suff col_y_sup : has_sup (col y).
+      move: col_y_sup => /sup_upper_bound.
+      by apply; exact/imageT.
+    split; first exact: col_nonempty.
+    by exists (sup rows).
+  move: cols_sup => /sup_upper_bound.
+  by apply; exact/imageT.
+- apply: ge_sup; first by have [] := cols_sup.
+  by move=> _ [y _ <-]; exact: col_le_rows.
+Qed.
 
-Lemma __admitted__interchange_sup (S : T -> U -> R) :
-    (forall x, has_sup [set r | exists y, r = S x y])
-  -> has_sup [set r | exists x, r = sup [set r | exists y, r = S x y]]
-  -> sup [set r | exists x, r = sup [set r | exists y, r = S x y]]
-  = sup [set r | exists y, r == sup [set r | exists x, r = S x y]].
-Proof using Type. Admitted.
 End SupInterchange.
 
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="lacks proof, use __admitted__interchange_sup explicitly if you really want to use this lemma")]
-Notation interchange_sup := __admitted__interchange_sup.
+#[deprecated(since="1.17.0", note="use `interchange_sup` instead")]
+Notation __admitted__interchange_sup := interchange_sup (only parsing).
 
 (* -------------------------------------------------------------------- *)
 Section PSumInterchange.
 Context {R : realType} {T U : choiceType}.
 
-Lemma __admitted__interchange_psum (S : T -> U -> R) :
-    (forall x, summable (S x))
-  -> summable (fun x => PosSum.psum (fun y => S x y))
-  -> PosSum.psum (fun x => PosSum.psum (fun y => S x y)) = PosSum.psum (fun y => PosSum.psum (fun x => S x y)).
-Proof using Type. Admitted.
+Lemma interchange_psum (S : T -> U -> R) : (forall x, summable (S x)) ->
+    summable (fun x => PosSum.psum (fun y => S x y)) ->
+  PosSum.psum (fun x => PosSum.psum (fun y => S x y)) =
+  PosSum.psum (fun y => PosSum.psum (fun x => S x y)).
+Proof.
+move=> row_summable rows_summable.
+pose P := fun xy : T * U => S xy.1 xy.2.
+have sumP : summable P.
+  apply: summable_pair_from_rows_psum.
+  - exact: row_summable.
+  - exact: eq_summable rows_summable.
+by rewrite -[LHS](psum_pair sumP)// [LHS](psum_pair_swap sumP).
+Qed.
+
 End PSumInterchange.
 
-#[deprecated(since="mathcomp-analysis 0.6.2",
-  note="lacks proof, use __admitted__interchange_psum explicitly if you really want to use this lemma")]
-Notation interchange_psum := __admitted__interchange_psum.
+#[deprecated(since="1.17.0", note="use `interchange_psum` instead")]
+Notation __admitted__interchange_psum := interchange_psum (only parsing).
 
 (* -------------------------------------------------------------------- *)
 Section SumTheory.