diff --git a/coq/utils/ListAdd.v b/coq/utils/ListAdd.v
index e7acbf7b..50ccebea 100644
--- a/coq/utils/ListAdd.v
+++ b/coq/utils/ListAdd.v
@@ -1070,6 +1070,20 @@ Section combining.
 
 End combining.
 
+Lemma fst_split {A B:Type} (l:list (A*B)) : fst (List.split l) = map fst l.
+Proof.
+  induction l; simpl; trivial.
+  destruct a; destruct (List.split l); simpl in *.
+  congruence.
+Qed.
+
+Lemma snd_split {A B:Type} (l:list (A*B)) : snd (List.split l) = map snd l.
+Proof.
+  induction l; simpl; trivial.
+  destruct a; destruct (List.split l); simpl in *.
+  congruence.
+Qed.
+
 Definition adjacent_pairs {A:Type} (l:list A) := (combine l (tl l)).
 
 Definition adjacent_pairs_alt {A:Type} (l:list A) := (combine (removelast l) (tl l)).
diff --git a/coq/utils/RealAdd.v b/coq/utils/RealAdd.v
index 6b3b0d8a..053e3a18 100644
--- a/coq/utils/RealAdd.v
+++ b/coq/utils/RealAdd.v
@@ -4106,6 +4106,27 @@ Proof.
   now apply Rle_max_compat_l.
 Qed.
 
+Lemma max_min_list_s (l : list (R * R)) : l <> nil ->
+ let '(l1, l2) := split l in
+  Rabs ((Rmin_list l1) - (Rmin_list l2)) <=
+    Rmax_list (map (fun '(x,y) => Rabs(x - y)) l).
+Proof.
+  generalize (max_min_list l).
+  rewrite <- fst_split, <- snd_split.
+  destruct (split l); trivial.
+Qed.
+
+Lemma max_min_list2 (l1 l2 : list R) : l1 <> nil -> length l1 = length l2 ->
+  Rabs ((Rmin_list l1) - (Rmin_list l2)) <=
+    Rmax_list (map (fun '(x,y) => Rabs(x - y)) (combine l1 l2)).
+Proof.
+  intros nnil eqlen.
+  generalize (max_min_list_s (combine l1 l2)).
+  rewrite combine_split; trivial; intros HH.
+  rewrite HH; [reflexivity |].
+  destruct l1; destruct l2; simpl in *; congruence.
+Qed.
+
 End Rmax_list.
 
 Notation "Max_{ l } ( f )" := (Rmax_list (List.map f l)) (at level 50) : rmax_scope.