diff --git a/coq/ProbTheory/Martingale.v b/coq/ProbTheory/Martingale.v
index 767e0ca7..d209eb34 100644
--- a/coq/ProbTheory/Martingale.v
+++ b/coq/ProbTheory/Martingale.v
@@ -2644,6 +2644,7 @@ Proof.
     apply Rmax_r.
 Qed.
 
+(*
 Lemma double_series_interchange (f : nat -> nat -> R) :
   (forall n m, 0 <= f n m) ->
   Series (fun n => Series (fun m => f n m)) =
@@ -2677,8 +2678,6 @@ Proof.
   rewrite <- ex_series_Lim_seq.  
   
   
-  Admitted.
-
 Lemma zerotails_eps2k_double_sum_eq (a : nat -> R) (pf:ex_series a) {anneg:NonnegativeFunction a}:
   Series (fun k => Series (fun x => a (S (x+ (zerotails_eps2k_fun a pf k)%nat)))) =
     Series (fun n => zerotails_incr_mult a pf n * (a n)).
@@ -2722,4 +2721,4 @@ Proof.
   now rewrite Rmult_comm.
  Qed.
 
-  
+  *)
diff --git a/coq/utils/RbarAdd.v b/coq/utils/RbarAdd.v
index 8a58c115..beded618 100644
--- a/coq/utils/RbarAdd.v
+++ b/coq/utils/RbarAdd.v
@@ -1025,7 +1025,7 @@ Qed.
           now apply sum_Rbar_n_nneg_nneg.
   Qed.
 
-
+(*
   (* Fubini for nonnegative reals *)
   Lemma Series_Series_seq_pair (f:nat->nat->R) :
     (forall a b, 0 <= (f a b)) ->
@@ -1034,7 +1034,7 @@ Qed.
   Proof.
     intros.
     apply Rle_antisym.
-Admitted.
+*)
 (*
     - apply Elim_seq_le_bound; intros.
       replace (sum_Rbar_n
@@ -1331,7 +1331,7 @@ Admitted.
     - now intros.
     - now intros.
   Qed.
-
+(*
   Lemma Series_nneg_nested_swap (f:nat->nat->R) :
     (forall a b, 0 <= (f a b)) ->
     Series (fun i : nat => Series (fun j : nat => (f i j))) =
@@ -1341,7 +1341,7 @@ Admitted.
     rewrite Series_Series_seq_pair.
     rewrite Series_Series_seq_pair.
     - apply Rle_antisym.
-      + Admitted.
+*)
   (*
         apply Elim_seq_le_bound; intros.
         destruct (sum_Rbar_n_iso_swap f n H).