diff --git a/CaseStudies/Gathering/InR2/Weber/Line.v b/CaseStudies/Gathering/InR2/Weber/Line.v
index 6b2a93a4f1a550869f4fb3d4a9c30dc3dba81456..f19784f84971591507506117d7b4a27704247959 100644
--- a/CaseStudies/Gathering/InR2/Weber/Line.v
+++ b/CaseStudies/Gathering/InR2/Weber/Line.v
@@ -1018,6 +1018,67 @@ Proof.
 unfold line_right. rewrite line_P_iP_max, (@filter_nilA _ equiv) ; [| autoclass | now intros ? ? ->].
 intros x Hin. rewrite Rltb_false. apply Rle_not_lt. now apply line_bounds.
 Qed.
+
+Lemma line_reverse_left L w ps:
+  eqlistA equiv
+    ((line_reverse L)^left w ps)
+    ((L^right) w ps).
+Proof.
+  unfold line_left , line_right.
+  apply filter_extensionalityA_compat.
+  2:reflexivity.
+  red.
+  intros x y heqxy. 
+  rewrite heqxy.
+  rewrite 2 line_reverse_proj.
+  destruct (Rltb ((L ^P) w) ((L ^P) y)) eqn:heq.
+  - rewrite Rltb_true in *|-*.
+    lra.
+  - rewrite Rltb_false in *|-*.
+    lra.
+Qed.
+
+Lemma line_reverse_right L w ps:
+  eqlistA equiv
+    ((line_reverse L)^right w ps)
+    ((L^left) w ps).
+Proof.
+  unfold line_left , line_right.
+  apply filter_extensionalityA_compat.
+  2:reflexivity.
+  red.
+  intros x y heqxy.
+  rewrite heqxy.
+  rewrite 2 line_reverse_proj.
+  destruct (Rltb ((L ^P) y) ((L ^P) w)) eqn:heq.
+  - rewrite Rltb_true in *|-*.
+    lra.
+  - rewrite Rltb_false in *|-*.
+    lra.
+Qed.
+
+Lemma line_reverse_on L w ps:
+  eqlistA equiv
+    ((line_reverse L)^on w ps)
+    ((L^on) w ps).
+Proof.
+  unfold line_on.
+  apply filter_extensionalityA_compat.
+  2:reflexivity.
+  red.
+  intros x y heqxy.
+  rewrite heqxy.
+  rewrite 2 line_reverse_proj.
+  destruct (((L ^P) w) ==b ((L ^P) y)) eqn:heq.
+  - rewrite eqb_true_iff in *|-*.
+    rewrite heq.
+    reflexivity.
+  - rewrite eqb_false_iff in *|-*.
+    cbn  .
+    cbn in heq.
+    lra.
+Qed.
+
   
 Lemma bipartition_min: forall L ps,
     PermutationA equiv ps
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index b28ce7b071b7701902cf82eeb8f006364e122c6c..116accba6c39d8d147d3d4599dcfa6a1f954e184 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -2090,7 +2090,7 @@ Proof.
       
       line_left_spec.
 
-    }
+    
     apply eqlistA_PermutationA.
     rewrite eqlistA_app.
     4:assumption.
@@ -2137,16 +2137,206 @@ Proof.
 Admitted.
 
 *)
+
+Lemma weber_aligned_sufficient L ps w : 
+  ps <> nil ->                  (* Seems necessary *)
+  line_dir L =/= 0%VS ->
+  aligned_on L (w :: ps) -> 
+  ((^R (L^right w ps)) - (^R (L^left w ps)) = ^R (L^on w ps))%R ->
+  ((^R (L^left w ps)) - (^R (L^right w ps)) < 0)%R ->
+  Weber ps (L^-P (L^min (L^right w ps))).
+Proof.
+  intros Hpsnonnil Hlinedir Halign H_eq_on H_right. 
+  remember (L^-P (L^min (L^right w ps))) as w'.
+  assert(InA equiv w' ((L ^right) w ps)) as h_InA.
+  { subst w'.
+    apply line_iP_min_InA.
+    - rewrite <- length_zero_iff_nil.
+
+      assert (0 <= (INR (length (line_left L w ps))))%R. 
+      { apply pos_INR. }
+      assert (INR (length (line_right L w ps)) > 0)%R as h_lgth.
+      { lra. }
+      intro abs.
+      rewrite  abs in h_lgth.
+      cbn in h_lgth.
+      lra.
+    - eapply aligned_on_inclA with (ps':=ps).
+      + apply line_right_inclA.
+      + rewrite aligned_on_cons_iff in Halign.
+        apply Halign. }
+  specialize (bipartition_min L ((L ^right) w ps)) as h.
+  apply PermutationA_length in h.
+  rewrite app_length in h.
+  (* apply (f_equal INR) in h. *)
+  (* rewrite plus_INR in h. *)
+  (* rewrite <- Heqw' in h. *)
+  rewrite <- Heqw' in h.
+
+  specialize (line_left_on_right_partition L w ps) as h_w.
+  specialize (line_left_on_right_partition L w' ps) as h_w'.
+  rewrite h_w' in h_w at 1.
+  clear h_w'.
+  apply PermutationA_length in h_w.
+  rewrite 4 app_length in h_w.
+  rewrite weber_aligned_spec_weak with (L:=L);auto.
+  2:{ rewrite aligned_on_cons_iff in *|-*.
+      split.
+      - subst w'.
+        apply line_contains_proj_inv.
+        assumption.
+      - apply Halign. }
+  
+  assert ((L ^P) w < (L ^P) w')%R.
+  { subst w'.
+    rewrite line_P_iP_min.
+    (* TODO: have a lemma *)
+    unfold line_right in h_InA at 2.
+    apply filter_InA in h_InA.
+    2:{ intros ? ? h_eq.
+        f_equal.
+        now rewrite h_eq. }
+    rewrite Rltb_true in h_InA.
+    rewrite line_P_iP_min in h_InA.            
+    apply h_InA. }
+  rewrite <- aggravate_right in h;auto.
+  rewrite <- aggravate_on in h;auto.
+  rewrite <- h in h_w.
+  apply (f_equal INR) in h, h_w.
+  rewrite plus_INR in h,h_w.
+  rewrite plus_INR in h_w.
+  rewrite plus_INR in h_w.
+  (* rewrite <- Heqw' in h. *)
+  assert (((^R (L ^left) w' ps) - (^R (L ^right) w' ps)) = (^R (L ^on) w' ps))%R.
+  { lra. }
+  assert (0 <= (^R (L ^on) w' ps))%R.
+  { apply pos_INR. }
+  rewrite Rabs_pos_eq;
+    lra.
+Qed.
+
+
+Lemma weber_aligned_single_weber_sufficient L ps w : 
+  ps <> nil ->                  (* Seems necessary *)
+  line_dir L =/= 0%VS ->
+  aligned_on L (w :: ps) -> 
+  ((^R (L^right w ps)) - (^R (L^left w ps)) = ^R (L^on w ps))%R ->
+  ((^R (L^left w ps)) - (^R (L^right w ps)) < 0)%R ->
+  ~ OnlyWeber ps w.
+Proof.
+  intros Hpsnonnil Hlinedir Halign H_eq_on H_right. 
+  intro abs.
+  remember (L^-P (L^min (L^right w ps))) as w'.
+  assert (Weber ps w') as Hweberw'.
+  { subst.
+    apply weber_aligned_sufficient;auto. }
+  assert(InA equiv w' ((L ^right) w ps)) as h_w_right.
+  { subst w'.
+    apply line_iP_min_InA.
+    - rewrite <- length_zero_iff_nil.
+
+      assert (0 <= (INR (length (line_left L w ps))))%R. 
+      { apply pos_INR. }
+      assert (INR (length (line_right L w ps)) > 0)%R as h_lgth.
+      { lra. }
+      intro abs3.
+      rewrite abs3 in h_lgth.
+      cbn in h_lgth.
+      lra.
+    - eapply aligned_on_inclA with (ps':=ps).
+      + apply line_right_inclA.
+      + rewrite aligned_on_cons_iff in Halign.
+        apply Halign. }
+  assert (abs2:w'<>w).
+  { specialize (line_right_spec L w w' ps) as h.
+    red in abs.
+    rewrite h in h_w_right.
+    intro abs4.
+    rewrite  abs4 in h_w_right.
+    lra. }
+  apply abs2.
+  now apply abs.
+Qed.
+
+
+(* there is at least one point in ps at the right of w. Let us
+   take the closest one p. hypothesis (left w - right w = on w)
+   implies that the point w' = (w+p)/2 is such that: (left w' -
+   right w' = 0 = on w') because left w' = left w + on w, and
+   right w' = right w. so by 1st order spec w' is a weber point
+   distinct from w, which contradict OnlyWeber w. *)
+
+Lemma weber_aligned_spec_right L ps w : 
+  ps <> nil ->                  (* Seems necessary *)
+  line_dir L =/= 0%VS ->
+  aligned_on L (w :: ps) -> 
+  ((^R (L^left w ps)) - (^R (L^right w ps)) < 0)%R ->
+  OnlyWeber ps w -> 
+    (Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R.
+Proof. 
+  intros Hpsnonnil Hlinedir Halign H_right HonlyWeber. 
+  specialize (weber_aligned_spec_weak Hlinedir Halign) as h_weak. 
+  destruct (HonlyWeber) as [hweber honly].
+  apply h_weak in hweber.
+  destruct (Rle_lt_or_eq_dec _ _ hweber) as [hlt | h_exact];clear hweber.
+    + auto.
+    + exfalso.
+      apply (@weber_aligned_single_weber_sufficient L ps w);auto.
+      rewrite Rabs_left in h_exact.
+      lra.
+      assumption.
+Qed.
+
+Lemma weber_aligned_spec_left L ps w : 
+  ps <> nil ->                  (* Seems necessary *)
+  line_dir L =/= 0%VS ->
+  aligned_on L (w :: ps) -> 
+  ((^R (L^right w ps)) - (^R (L^left w ps)) < 0)%R ->
+  OnlyWeber ps w -> 
+    (Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R.
+Proof. 
+  intros Hpsnonnil Hlinedir Halign H_right HonlyWeber. 
+  specialize (weber_aligned_spec_weak Hlinedir Halign) as h_weak. 
+  destruct (HonlyWeber) as [hweber honly].
+  apply h_weak in hweber.
+  destruct (Rle_lt_or_eq_dec _ _ hweber) as [hlt | h_exact];clear hweber.
+    + auto.
+    + exfalso.
+      
+      apply (@weber_aligned_single_weber_sufficient (line_reverse L) ps w);auto.
+      * cbn -[opp equiv].
+        intros abs.
+        rewrite <- opp_origin in abs.
+        apply opp_reg in abs.
+        contradiction.
+      * now rewrite <- aligned_on_reverse.
+      * rewrite line_reverse_right, line_reverse_left,line_reverse_on.
+        rewrite Rabs_right in h_exact.
+        -- lra.
+        -- lra.
+      * now rewrite line_reverse_right, line_reverse_left.
+Qed.
+
+
+
+
 Lemma weber_aligned_spec L ps w : 
   ps <> nil ->                  (* Seems necessary *)
   line_dir L =/= 0%VS ->
   aligned_on L (w :: ps) -> 
-    OnlyWeber ps w <-> 
+    OnlyWeber ps w -> 
     (Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R.
     (* (Rabs (INR (length (L^left w ps)) - INR (length (L^right w ps))) < INR (length (L^on w ps)))%R. *)
 Proof. 
   intros Hpsnonnil Hlinedir Halign. 
   specialize (weber_aligned_spec_weak Hlinedir Halign) as h_weak. 
+  destruct
+    (Rcase_abs ((^R (L ^left) w ps)
+                - (^R (L ^right) w ps))%R) as [h_abs| h_abs].
+  - apply weber_aligned_spec_right;auto.
+  - specialize (@weber_aligned_spec_right (line_reverse L) ps) as hrev.
+
+
   split.
   - intros H.
     destruct H.
@@ -2160,9 +2350,13 @@ Proof.
          (left w' - right w' = 0 = on w') because left w' = left w + on w, and right w' = right w.
          so by 1st order spec w' is a weber point distinct from w, which contradict OnlyWeber w. *)
       (* First get rid of the Rabs ,by distinguishing the two cases *)
-      destruct (Rcase_abs ((^R (L ^left) w ps) - (^R (L ^right) w ps))%R) as [h_abs| h_abs];
-        [ rewrite (Rabs_left _ h_abs) in h_exact | rewrite (Rabs_right _ h_abs) in h_exact].
-      * remember (L^-P (L^min (L^right w ps))) as w'.
+      destruct
+        (Rcase_abs ((^R (L ^left) w ps)
+                    - (^R (L ^right) w ps))%R) as [h_abs| h_abs];
+        [ rewrite (Rabs_left _ h_abs) in h_exact |
+          rewrite (Rabs_right _ h_abs) in h_exact].
+      * 
+        remember (L^-P (L^min (L^right w ps))) as w'.
         assert(InA equiv w' ((L ^right) w ps)).
         { subst w'.
           apply line_iP_min_InA.
@@ -2203,30 +2397,126 @@ Proof.
                 assumption.
               - apply Halign. }
           
-          rewrite <- aggravate_right in h.
-          rewrite <- aggravate_on in h.
-          lia.
-
-
-          assert( (Rlength ((L ^left) w' ps)) = (Rlength ((L ^left) w ps)) + (Rlength ((L ^on) w ps))).
-          { rewrite h in h_w.
-
+          assert ((L ^P) w < (L ^P) w')%R.
+          { subst w'.
+            rewrite line_P_iP_min.
+            (* TODO: have a lemma *)
+            assert(InA equiv (L^-P ((L ^min) ((L ^right) w ps)))
+                     ((L ^right) w ps)).
+            { admit. }
+            unfold line_right in H1 at 2.
+            apply filter_InA in H1.
+            2:{ repeat intro.
+                f_equal.
+                now rewrite H3. }
+            rewrite Rltb_true in H1.
+            rewrite line_P_iP_min in H1.            
+            apply H1.
+          }
+          rewrite <- aggravate_right in h;auto.
+          rewrite <- aggravate_on in h;auto.
+          rewrite <- h in h_w.
+          apply (f_equal INR) in h, h_w.
+          rewrite plus_INR in h,h_w.
+          rewrite plus_INR in h_w.
+          rewrite plus_INR in h_w.
+          (* rewrite <- Heqw' in h. *)
+          assert (((^R (L ^left) w' ps) - (^R (L ^right) w' ps)) = (^R (L ^on) w' ps))%R.
+          { lra. }
+          assert (0 <= (^R (L ^on) w' ps))%R.
+          { apply pos_INR. }
+          rewrite Rabs_pos_eq;
+          lra. }
+        assert (abs:w'<>w).
+        { specialize (line_right_spec L w w' ps) as h.
+          rewrite h in H.
+          intro abs.
+          rewrite  abs in H.
+          lra. }
+        apply abs.
+        now apply H0.
+      * remember (L^-P (L^min (L^right w ps))) as w'.
+        assert(InA equiv w' ((L ^right) w ps)).
+        { subst w'.
+          apply line_iP_min_InA.
+          - rewrite <- length_zero_iff_nil.
 
-            
-            lra. admit. }
-          lra.
+            assert (0 <= (INR (length (line_left L w ps))))%R. 
+            { apply pos_INR. }
+            assert (INR (length (line_right L w ps)) > 0)%R as h_lgth.
+            { lra.  }
+            intro abs.
+            rewrite  abs in h_lgth.
+            cbn in h_lgth.
+            lra.
+          - eapply aligned_on_inclA with (ps':=ps).
+            + apply line_right_inclA.
+            + rewrite aligned_on_cons_iff in Halign.
+              apply Halign. }
+        assert(Weber ps w').
+        { specialize (bipartition_min L ((L ^right) w ps)) as h.
+          apply PermutationA_length in h.
+          rewrite app_length in h.
+          (* apply (f_equal INR) in h. *)
+          (* rewrite plus_INR in h. *)
+          (* rewrite <- Heqw' in h. *)
+          rewrite <- Heqw' in h.
 
-          rewrite Rabs_pos_eq.
-          { lra.
-        }
+          specialize (line_left_on_right_partition L w ps) as h_w.
+          specialize (line_left_on_right_partition L w' ps) as h_w'.
+          rewrite h_w' in h_w at 1.
+          clear h_w'.
+          apply PermutationA_length in h_w.
+          rewrite 4 app_length in h_w.
+          rewrite weber_aligned_spec_weak with (L:=L);auto.
+          2:{ rewrite aligned_on_cons_iff in *|-*.
+              split.
+              - subst w'.
+                apply line_contains_proj_inv.
+                assumption.
+              - apply Halign. }
+          
+          assert ((L ^P) w < (L ^P) w')%R.
+          { subst w'.
+            rewrite line_P_iP_min.
+            (* TODO: have a lemma *)
+            assert(InA equiv (L^-P ((L ^min) ((L ^right) w ps)))
+                     ((L ^right) w ps)).
+            { admit. }
+            unfold line_right in H1 at 2.
+            apply filter_InA in H1.
+            2:{ repeat intro.
+                f_equal.
+                now rewrite H3. }
+            rewrite Rltb_true in H1.
+            rewrite line_P_iP_min in H1.            
+            apply H1.
+          }
+          rewrite <- aggravate_right in h;auto.
+          rewrite <- aggravate_on in h;auto.
+          rewrite <- h in h_w.
+          apply (f_equal INR) in h, h_w.
+          rewrite plus_INR in h,h_w.
+          rewrite plus_INR in h_w.
+          rewrite plus_INR in h_w.
+          (* rewrite <- Heqw' in h. *)
+          assert (((^R (L ^left) w' ps) - (^R (L ^right) w' ps)) = (^R (L ^on) w' ps))%R.
+          { lra. }
+          assert (0 <= (^R (L ^on) w' ps))%R.
+          { apply pos_INR. }
+          rewrite Rabs_pos_eq;
+          lra. }
         assert (abs:w'<>w).
         { specialize (line_right_spec L w w' ps) as h.
-          rewrite h in H1.
+          rewrite h in H.
           intro abs.
-          rewrite  abs in H1.
+          rewrite  abs in H.
           lra. }
         apply abs.
         now apply H0.
+
+
+      *
       *