From 166087dcdfb35d5ea9d97f37a0d7e4777f4bf530 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Mon, 27 Jan 2025 08:49:54 -0500
Subject: [PATCH] cleanup

---
 coq/QLearn/Tsitsiklis.v | 13 -------------
 coq/utils/RealAdd.v     | 14 ++++++++++++++
 2 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/coq/QLearn/Tsitsiklis.v b/coq/QLearn/Tsitsiklis.v
index 50334464..be62fca3 100644
--- a/coq/QLearn/Tsitsiklis.v
+++ b/coq/QLearn/Tsitsiklis.v
@@ -10535,19 +10535,6 @@ End FixedPoint_contract.
     
   Existing Instance Rbar_le_pre.
 
-  Lemma fold_left_Rmax_abs l : List.Forall (Rle 0) l -> fold_left Rmax l 0 = Rmax_list l.
-  Proof.
-    intros.
-    rewrite fold_symmetric.
-    - induction l; simpl; trivial.
-      invcs H.
-      rewrite IHl; trivial.
-      destruct l; simpl; trivial.
-      rewrite Rmax_left; trivial.
-    - apply Rmax_assoc.
-    - apply Rmax_comm.
-  Qed.
-
   Instance finfun_sa : SigmaAlgebra (Rfct (sigT M.(act))) :=
     iso_sa (iso := Isomorphism_symm (finite_fun_vec_encoder finA EqDecsigT (B := R)))
       (Rvector_borel_sa _).
diff --git a/coq/utils/RealAdd.v b/coq/utils/RealAdd.v
index d5c5d38b..4ee9811e 100644
--- a/coq/utils/RealAdd.v
+++ b/coq/utils/RealAdd.v
@@ -3321,6 +3321,20 @@ Section Rmax_list.
     - assumption.
   Qed.
 
+  Lemma fold_left_Rmax_abs l : List.Forall (Rle 0) l -> fold_left Rmax l 0 = Rmax_list l.
+  Proof.
+    intros.
+    rewrite fold_symmetric.
+    - induction l; simpl; trivial.
+      invcs H.
+      rewrite IHl; trivial.
+      destruct l; simpl; trivial.
+      rewrite Rmax_left; trivial.
+    - apply Rmax_assoc.
+    - apply Rmax_comm.
+  Qed.
+
+
   Definition Rmax_list_map {A} (l : list A) (f : A -> R) := Rmax_list (List.map f l).
   Definition Rmin_list_map {A} (l : list A) (f : A -> R) := Rmin_list (List.map f l).