From 51ea3d62be319b2b14aac4ac6c1c81d47aac1eeb Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Tue, 5 Nov 2024 15:10:45 +0100
Subject: [PATCH] several more admits removed.

---
 .../Gathering/InR2/Weber/Gather_flex_async.v  | 202 ++++++--
 CaseStudies/Gathering/InR2/Weber/Line.v       | 199 +++++++-
 .../Gathering/InR2/Weber/Weber_point.v        | 477 +++++++++++++++++-
 3 files changed, 814 insertions(+), 64 deletions(-)

diff --git a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
index c2706e18..441f5198 100644
--- a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
+++ b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
@@ -37,7 +37,6 @@ Require Import Psatz.
 Require Import Inverse_Image.
 Require Import FunInd.
 Require Import FMapFacts.
-(* Require Import LibHyps.LibHyps. *)
 Require Import Pactole.Util.ListComplements.
 (* Helping typeclass resolution avoid infinite loops. *)
 (* This does not seem to help much *)
@@ -112,16 +111,21 @@ Local Existing Instance weber_calc_compat.
 (* We then build a function that calculates the weber segment of a set of points. *)
 Definition weber_calc_seg : list R2 -> R2 * R2. Admitted.
 
-Lemma weber_calc_seg_correct : forall ps w,
-    ps <> [] ->
+Lemma weber_calc_seg_correct : forall ps,
+    ps <> [] -> forall w,
     let '(w1, w2) := weber_calc_seg ps in 
     Weber ps w <-> segment w1 w2 w.
 Proof. Admitted.
-
-Lemma weber_calc_seg_correct_2 : forall ps w,
-    let '(w1, w2) := weber_calc_seg ps in 
-    segment w1 w2 w -> Weber ps w.
-Proof. Admitted.
+Lemma weber_calc_seg_correct_1 : forall ps w1 w2,
+    ps <> [] ->
+    weber_calc_seg ps = (w1, w2) -> 
+    forall w, Weber ps w <-> segment w1 w2 w.
+Proof. 
+  intros ps w1 w2 H H0 w. 
+  specialize (weber_calc_seg_correct H ) as h.
+  rewrite H0 in h.
+  apply h.
+Qed.
 
 Lemma weber_calc_seg_compat : Proper (PermutationA equiv ==> perm_pairA equiv) weber_calc_seg.
 Proof. Admitted.
@@ -316,6 +320,16 @@ Proof using lt_0n.
   lia.
 Qed.
 
+
+Lemma weber_calc_seg_correct_2 : forall c w1 w2,
+    weber_calc_seg (pos_list c) = (w1, w2) -> 
+    forall w, Weber (pos_list c) w <-> segment w1 w2 w.
+Proof.
+  intros c w1 w2 H w. 
+  apply weber_calc_seg_correct_1;auto.
+  apply pos_list_non_nil.
+Qed.
+
 (* This would have been much more pleasant to do with mathcomp's tuples. *)
 Lemma config_list_InA_combine x x' (c c':configuration) : 
   InA equiv (x, x') (combine (config_list c) (config_list c')) <-> 
@@ -708,18 +722,18 @@ Proof using Type.
 Qed.
 
 
-Lemma invalid_config_obs: forall c,
-    invalid c <-> forall info, invalid_obs ((obs_from_config c info)).
+Lemma invalid_config_obs: forall c info, 
+    invalid c <-> invalid_obs ((obs_from_config c info)).
 Proof using Type.
-  intros c.
-  split;[intros h i | intros h].
+  intros c i.
+  split;[intros h | intros h].
   - red in h .
     decompose [ex and] h. clear h.
     red.
     rewrite n_cardinal.
     exists x , x0;intuition.
   - red.
-    specialize (h (0%VS, 0%VS, ratio_0)).
+    (* specialize (h (0%VS, 0%VS, ratio_0)). *)
     red in h.
     decompose [ex and] h. clear h.
     rewrite n_cardinal in H1, H3.
@@ -2189,10 +2203,12 @@ assert (Proper (equiv ==> equiv) (projT1 f)) as f_compat.
 { unfold f ; cbn -[equiv]. intros x y Hxy ; now rewrite Hxy. }
 unfold gatherW_pgm at 1. pose (sim := change_frame da config g). foldR2. fold sim.
 cbn -[segment_decb strict_segment_decb middle robot_with_mult Nat.div sim
-  config_list get_location multi_support equiv_dec line_proj line_proj_inv] ; repeat split ; [].
+  config_list get_location multi_support equiv_dec line_proj line_proj_inv cardinal] ; repeat split ; [].
 apply (Similarity.injective sim). rewrite Bijection.section_retraction. foldR2.
 
 
+
+
 specialize weber_calc_seg_correct with (1:=(pos_list_non_nil config)) as Hw.
 destruct (weber_calc_seg (pos_list config)) as [w1 w2].
 foldR2.
@@ -2229,9 +2245,9 @@ assert (Hmiddle : aligned (pos_list config) -> middle r1' r2' = sim (middle r1 r
   intros Hnil. apply (f_equal (@length R2)) in Hnil. rewrite pos_list_length in Hnil. cbn in Hnil. lia.
 }
 
-assert (Hmult : robot_with_mult (Nat.div2 (n+1)) (multi_support obs) == option_map sim (robot_with_mult (Nat.div2 (n+1)) (pos_list config))).
-{
-  apply (@option_map_injective _ _ _ _ (inverse sim)) ; try apply Similarity.injective ; [].
+assert (Hmult : robot_with_mult (Nat.div2 (cardinal obs+1)) (multi_support obs) == option_map sim (robot_with_mult (Nat.div2 (n+1)) (pos_list config))).
+{ admit.
+(*  apply (@option_map_injective _ _ _ _ (inverse sim)) ; try apply Similarity.injective ; [].
   rewrite option_map_map. setoid_rewrite option_map_id at 2.
   2: now intros x ; cbn ; rewrite Bijection.retraction_section. 
   rewrite robot_with_mult_map ; [| | now apply Similarity.injective].
@@ -2241,7 +2257,7 @@ assert (Hmult : robot_with_mult (Nat.div2 (n+1)) (multi_support obs) == option_m
     setoid_rewrite <-List.map_id at 1. apply eqlistA_PermutationA. f_equiv.
     intros ? ? H. cbn -[sim get_location].
     rewrite H. foldR2. fold sim. now rewrite Bijection.retraction_section.
-  + intros ? ? H. cbn. now rewrite H.
+  + intros ? ? H. cbn. now rewrite H. *)
 }
 
 assert (Hcenter : 0%VS == sim (get_location (config (Good g)))).
@@ -2275,15 +2291,23 @@ assert (Hweb_align : w1 =/= w2 -> aligned (pos_list config)).
   + rewrite Hw. apply segment_start.
 }
 
-case Hw_perm as [[<- <-] | [<- <-]].
-+ case ifP_sumbool ; case ifP_sumbool ; intros Hw' Hw_sim.
+destruct (obs_invalid_dec obs) at 1.
+{ exfalso.
+  admit. }
+destruct (length (multi_support obs)).
+{ admit. }
+cbn [ equiv_dec nat_EqDec Nat.eq_dec nat_rec nat_rect].
+
+case Hw_perm as [[<- <-] | [<- <-]]. 
++ case ifP_sumbool; case ifP_sumbool ; intros Hw' Hw_sim.
   - reflexivity.
   - exfalso. apply Hw'. now apply (Similarity.injective sim).
   - exfalso. apply Hw_sim. now f_equal.
   - foldR2. 
-    destruct (robot_with_mult (Nat.div2 (n+1)) (multi_support obs)) as [t|] ;
-    destruct (robot_with_mult (Nat.div2 (n+1)) (pos_list config)) as [t'|] ;
-      cbn in Hmult ; try now tauto.
+    destruct (robot_with_mult (Nat.div2 (cardinal obs+1)) (multi_support obs)) as [t|];
+    destruct (robot_with_mult (Nat.div2 (n+1)) (pos_list config)) as [t'|];
+      cbn [option_map] in Hmult ; try now tauto.
+    cbn [option_map] in Hmult.
     * rewrite Hmult, Hseg, Hcenter. now destruct_match.
     * repeat rewrite Hmiddle by auto. repeat rewrite Hseg_sim.
       repeat rewrite Hcenter. repeat rewrite Heq_sim.
@@ -2293,7 +2317,7 @@ case Hw_perm as [[<- <-] | [<- <-]].
   - exfalso. apply Hw'. now apply (Similarity.injective sim).
   - exfalso. apply Hw_sim. now f_equal.
   - foldR2. 
-    destruct (robot_with_mult (Nat.div2 (n+1)) (multi_support obs)) as [t|] ;
+    destruct (robot_with_mult (Nat.div2 (cardinal obs+1)) (multi_support obs)) as [t|] ;
     destruct (robot_with_mult (Nat.div2 (n+1)) (pos_list config)) as [t'|] ;
       cbn in Hmult ; try now tauto.
     * rewrite Hmult, Hseg, Hcenter. now destruct_match.
@@ -2313,7 +2337,7 @@ case Hw_perm as [[<- <-] | [<- <-]].
           rewrite <-segment_decb_false in Hm3. foldR2. rewrite Hm3.
           destruct_match ; reflexivity.
         --repeat destruct_match ; reflexivity.
-Qed.
+Admitted.
 
 (* This is the property : all robots are looping. 
  * This is what should be verified in the initial configuration. *)
@@ -2455,7 +2479,7 @@ Definition inv4 c L w1 w2 : Prop :=
 Lemma inv234_endpoints_distinct c L : 
   inv2 c L \/ (exists w1 w2, inv3 c L w1 w2) \/ (exists w1 w2, inv4 c L w1 w2) -> 
   L^-P (L^min (pos_list c)) =/= L^-P (L^max (pos_list c)).
-Proof using . 
+Proof using lt_0n. 
 intros Hinv234 Er12.
 assert (H : exists w1 w2,
   aligned_on L (pos_list c) /\
@@ -2463,9 +2487,14 @@ assert (H : exists w1 w2,
   w1 =/= w2).
 { case Hinv234 as [Hinv2 | [[w1 [w2 Hinv3]] | [w1 [w2 Hinv4]]]].
   + destruct Hinv2 as [Halign [NEw12 _]].
-    assert (Hweb := weber_calc_seg_correct (pos_list c)).
+    assert (Hweb := @weber_calc_seg_correct (pos_list c)).
     destruct (weber_calc_seg (pos_list c)) as [w1 w2]. 
-    now exists w1, w2.
+    exists w1, w2.
+    split;auto.
+    split;auto.
+    intros w. 
+    apply Hweb.
+    apply pos_list_non_nil.
   + destruct Hinv3 as [Halign [Hweb [NEw12 _]]]. now exists w1, w2.
   + destruct Hinv4 as [Halign [Hweb [Hseg _]]]. exists w1, w2.
     split ; [assumption | split ; [assumption|]].
@@ -2506,14 +2535,17 @@ transitivity x.
 + symmetry. rewrite <-good_unpack_good. apply Hgather.
 Qed. 
 
+
 (* In phases 3 and 4, the endpoints aren't weber points 
  * (because they have multiplicity < (n+1)/2). *)
 Lemma inv34_endpoints_not_weber c L w1 w2 : 
+  line_dir L <> 0%VS ->
   let ps := pos_list c in 
   inv3 c L w1 w2 \/ inv4 c L w1 w2 -> 
   ~Weber ps (L^-P (L^min ps)) /\ ~Weber ps (L^-P (L^max ps)).
 Proof using lt_0n. 
-cbn zeta. intros Hinv34.
+specialize (pos_list_non_nil c) as h_ps_nonnil.
+cbn zeta. intros Hnonnil Hinv34.
 pose (ps := pos_list c). pose (r1 := L^-P (L^min ps)). pose (r2 := L^-P (L^max ps)).
 assert (H :
   aligned_on L ps /\ 
@@ -2524,8 +2556,15 @@ assert (H :
 { case Hinv34 as [Hinv | Hinv] ; repeat split ; try apply Hinv. 
   destruct Hinv as [_ [_ [Hseg _]]]. intros ->. lra. }
 destruct H as [Halign [Hweb [NEw12 [Hr1_mult Hr2_mult]]]].
-fold ps r1 r2 in Hr1_mult, Hr2_mult |- *. split.
-+ intros Hr1_web. rewrite (weber_aligned_spec_weak _ Halign) in Hr1_web. 
+fold ps r1 r2 in Hr1_mult, Hr2_mult |- *.
+ split.
++ intros Hr1_web. 
+  assert (aligned_on L (r1::ps)) as Halign'.
+  { specialize (weber_aligned) as h.
+    apply aligned_on_cons_iff.
+    split;auto.
+    eapply h;eauto. }
+  rewrite (weber_aligned_spec_weak Hnonnil Halign') in Hr1_web. 
   assert (Hperm := line_left_on_right_partition L r1 ps).
   unfold r1 at 1 in Hperm. unfold r1 at 1 in Hr1_web. rewrite line_left_iP_min in Hperm, Hr1_web.
   cbn [app] in Hperm. cbn [length INR] in Hr1_web. 
@@ -2535,8 +2574,7 @@ fold ps r1 r2 in Hr1_mult, Hr2_mult |- *. split.
   assert (Hon : length (L^on r1 ps) < Nat.div2 (n+1)).
   { rewrite line_on_length_aligned.
     + unfold ps. now rewrite <-multiplicity_countA.
-    + rewrite aligned_on_cons_iff. split ; [apply Halign, line_iP_min_InA |] ; try assumption.
-      unfold ps. rewrite <-length_zero_iff_nil, pos_list_length. lia. }
+    + rewrite aligned_on_cons_iff. split ; [apply Halign, line_iP_min_InA |] ; try assumption. }
   assert (Hright : length (L^right r1 ps) < Nat.div2 (n+1)).
   { eapply Nat.le_lt_trans ; eauto. }
   case (Nat.Even_or_Odd n) as [[k Hk] | [k Hk]].
@@ -2545,7 +2583,13 @@ fold ps r1 r2 in Hr1_mult, Hr2_mult |- *. split.
   - rewrite Hk in Hon, Hright, Hperm.
     assert (Hrewrite : 2 * k + 1 + 1 = 2 * (k + 1)). { lia. }
     rewrite Hrewrite, Nat.div2_double in Hon, Hright. lia.
-+ intros Hr2_web. rewrite (weber_aligned_spec_weak _ Halign) in Hr2_web.
++ intros Hr2_web. 
+  assert (aligned_on L (r2::ps)) as Halign'.
+  { specialize (weber_aligned) as h.
+    apply aligned_on_cons_iff.
+    split;auto.
+    eapply h;eauto. }
+  rewrite (weber_aligned_spec_weak Hnonnil Halign') in Hr2_web.
   assert (Hperm := line_left_on_right_partition L r2 ps).
   unfold r2 at 3 in Hperm. unfold r2 at 2 in Hr2_web. rewrite line_right_iP_max in Hperm, Hr2_web.
   rewrite app_nil_r in Hperm. cbn [length INR] in Hr2_web. 
@@ -2555,8 +2599,7 @@ fold ps r1 r2 in Hr1_mult, Hr2_mult |- *. split.
   assert (Hon : length (L^on r2 ps) < Nat.div2 (n+1)).
   { rewrite line_on_length_aligned.
     + unfold ps. now rewrite <-multiplicity_countA.
-    + rewrite aligned_on_cons_iff. split ; [apply Halign, line_iP_max_InA |] ; try assumption.
-      unfold ps. rewrite <-length_zero_iff_nil, pos_list_length. lia. }
+    + rewrite aligned_on_cons_iff. split ; [apply Halign, line_iP_max_InA |] ; try assumption. }
   assert (Hleft : length (L^left r2 ps) < Nat.div2 (n+1)).
   { eapply Nat.le_lt_trans ; eauto. }
   case (Nat.Even_or_Odd n) as [[k Hk] | [k Hk]].
@@ -2664,24 +2707,31 @@ Lemma inv_initial c :
   (exists L w1 w2, inv3 c L w1 w2) \/ 
   (exists L w1 w2, inv4 c L w1 w2).
 Proof using lt_0n. 
-intros Hvalid Hstay. pose (ps := pos_list c).
-assert (Hweb := weber_calc_seg_correct ps).
+intros Hvalid Hstay.
+specialize weber_calc_seg_correct_2 with (c:=c) as Hweb.
+pose (ps := pos_list c).
+fold ps in Hweb.
+assert( ps <> []) as h_psnonnil.
+{ apply pos_list_non_nil. }
 destruct (weber_calc_seg ps) as [w1 w2] eqn:Ew.
+specialize (Hweb _ _ eq_refl).
 case (w1 =?= w2) as [Ew12 | NEw12].
 + (* Phase 1. *)  
-  left. exists w1. split ; [now apply config_stay_impl_config_stg|]. fold ps. split.
-  - rewrite Hweb. apply segment_start.
-  - intros x Hx. rewrite Hweb, <-Ew12, segment_same in Hx. exact Hx.
+  left. exists w1.
+  split ; [now apply config_stay_impl_config_stg|]. fold ps. split.
+  - apply Hweb. apply segment_start.
+  - intros x Hx. apply Hweb in Hx. rewrite <-Ew12, segment_same in Hx. exact Hx.
 + right. 
   assert (Halign : aligned ps).
   { case (aligned_dec (pos_list c)) as [Halign | HNalign] ; [assumption|].
     exfalso. apply NEw12. apply weber_Naligned_unique with (w := w1) in HNalign.
-    2: now fold ps ; rewrite Hweb ; apply segment_start.
+    2:{ fold ps ; rewrite Hweb.
+        - apply segment_start. }
     symmetry. apply HNalign. fold ps. rewrite Hweb. apply segment_end. }
   destruct Halign as [L Halign].
   assert (NEr12 : L^-P (L^min ps) =/= L^-P (L^max ps)).
   { intros Er12. apply (f_equal (L^P)) in Er12. rewrite line_P_iP_min, line_P_iP_max in Er12. apply NEw12. 
-    apply weber_segment_InA in Hweb. destruct Hweb as [Hw1_InA Hw2_InA].
+    specialize (weber_segment_InA Hweb) as Hweb'. destruct Hweb' as [Hw1_InA Hw2_InA].
     cut (L^P w1 == L^P w2).
     { intros Heq. apply (f_equal (L^-P)) in Heq. rewrite 2 Halign in Heq by assumption. exact Heq. }
     generalize (line_bounds L ps w1 Hw1_InA), (line_bounds L ps w2 Hw2_InA).
@@ -2708,7 +2758,11 @@ case (w1 =?= w2) as [Ew12 | NEw12].
       { intros Ht_web. apply NEw12. transitivity t.
         + apply Ht_web. rewrite Hweb. apply segment_start.
         + symmetry. apply Ht_web. rewrite Hweb. apply segment_end. }
-      rewrite weber_aligned_spec by exact Halign.
+      rewrite weber_aligned_spec with (L:=L);auto.
+      2:{ apply aligned_on_cons_iff.
+          split.
+          - apply aligned_on_InA_contains with (ps:=ps);auto.
+          - exact Halign. }
       assert (Hlr_bounds := @majority_left_right_bounds t c L Halign). 
       feed_n 2 Hlr_bounds.
       { rewrite multiplicity_countA. fold ps. rewrite Ht_mult. intuition. }
@@ -2836,8 +2890,9 @@ Proof using lt_0n delta_g0.
 intros Hinv Hsim. destruct (round_simplify Hsim (inv1_valid Hinv)) as [r Hround].
 exists r. rewrite Hround. intros id. destruct_match ; [|reflexivity].
 repeat split ; cbn [fst snd]. 
-assert (Hw12 := weber_calc_seg_correct (pos_list c)).
+assert (Hw12 := weber_calc_seg_correct_2 c).
 destruct (weber_calc_seg (pos_list c)) as [w1 w2].
+specialize (Hw12 w1 w2 eq_refl).
 assert (Hw1 : w1 == w).
 { apply Hinv. rewrite Hw12. apply segment_start. }
 assert (Hw2 : w2 == w).
@@ -2909,7 +2964,18 @@ destruct (robot_with_mult (Nat.div2 (n+1)) (pos_list c)) as [t2|] eqn:E.
 Qed.
 
 
+(* Ltac dolsps ps := *)
+(*   match goal with *)
+(*     H: let ps := _  |- _ => idtac H *)
+(*   end *)
+(* . *)
+Ltac fold_all t :=
+  (repeat progress match goal with
+      H  : _ |- _ => fold t in H
+    end); fold t.
+
 Lemma round_simplify_phase3 da c L w1 w2 :
+  line_dir L =/= 0%VS ->
   inv3 c L w1 w2 ->
   similarity_da_prop da ->
   exists (r : ident -> ratio),
@@ -2921,15 +2987,21 @@ Lemma round_simplify_phase3 da c L w1 w2 :
               in (get_location (c id), target, ratio_0)
             else inactive c id (r id).
 Proof using lt_0n delta_g0.
-intros Hinv3 Hsim. assert (Hvalid := inv3_valid Hinv3). 
+specialize (pos_list_non_nil c) as h_ps_nonnil.
+pose (ps := pos_list c).
+fold_all ps.
+intros HlineDir Hinv3 Hsim. assert (Hvalid := inv3_valid Hinv3). 
 destruct (round_simplify Hsim Hvalid) as [r Hround].
+fold_all ps.
 exists r. rewrite Hround. clear Hround. intros id. destruct_match ; [|reflexivity].
 repeat split ; cbn [fst snd]. 
 destruct Hinv3 as [Halign [Hweb [NEw12 [Hmiddle [Hstg [Hends [Hr1_mult Hr2_mult]]]]]]].
-assert (Hweb' := weber_calc_seg_correct (pos_list c)).
-destruct (weber_calc_seg (pos_list c)) as [w1' w2'].
+assert (Hweb' := weber_calc_seg_correct_2 c).
+fold_all ps.
+destruct (weber_calc_seg ps) as [w1' w2'].
+specialize (Hweb' w1' w2' eq_refl).
 assert (Hperm : perm_pairA equiv (w1', w2') (w1, w2)).
-{ apply segment_eq_iff. intros x. now rewrite <-Hweb', Hweb. }
+{ apply segment_eq_iff. intros x. now rewrite <-Hweb'. }
 case (w1' =?= w2') as [Ew12' | NEw12'].
 + exfalso. apply NEw12. case Hperm as [[H1 H2] | [H1 H2]].
   - rewrite <-H1, <-H2. exact Ew12'.
@@ -2948,22 +3020,39 @@ case (w1' =?= w2') as [Ew12' | NEw12'].
     { intros HOW. apply NEw12. transitivity t.
       * apply HOW. rewrite Hweb. apply segment_start.
       * symmetry. apply HOW. rewrite Hweb. apply segment_end. } 
-    rewrite (weber_aligned_spec _ Halign).
+    assert (aligned_on L (t::(pos_list c))) as halignt.
+    { apply aligned_on_cons_iff.
+      split.
+      - apply aligned_on_InA_contains with ps;auto.
+      - assumption. }
+    fold_all ps.
+    rewrite (weber_aligned_spec h_ps_nonnil HlineDir halignt).
     assert (Ht_line : line_contains L t).
     { apply Halign. rewrite <-multiplicity_pos_InA, multiplicity_countA, E.
       apply Exp_prop.div2_not_R0 ; lia. }
+    fold_all ps.
     rewrite line_on_length_aligned, E by now rewrite aligned_on_cons_iff.
     assert (Hlr_bounds := @majority_left_right_bounds t c L Halign).
     feed_n 2 Hlr_bounds.
-    { rewrite multiplicity_countA, E. intuition. }
-    { destruct (line_bounds L (pos_list c) t) as [[H1 | H2] [H3 | H4]] ; try assumption.
+    { rewrite multiplicity_countA. fold ps. rewrite E. intuition. }
+    { fold ps in Hr2_mult, Hr1_mult,Halign.
+      destruct (line_bounds L ps t) as [[H1 | H2] [H3 | H4]] ; try assumption.
       + tauto.
-      + exfalso. rewrite <-H4, Halign, multiplicity_countA, E in Hr2_mult by assumption. lia.
-      + exfalso. rewrite H2, Halign, multiplicity_countA, E in Hr1_mult by assumption. lia.
-      + exfalso. rewrite H2, Halign, multiplicity_countA, E in Hr1_mult by assumption. lia. } 
+      + exfalso. rewrite <-H4, Halign,multiplicity_countA (*, E*) in Hr2_mult by assumption.
+        fold ps in Hr2_mult.
+        rewrite E in Hr2_mult.
+        lia.
+      + exfalso. rewrite H2, Halign, multiplicity_countA in Hr1_mult by assumption.
+        fold ps in Hr1_mult.
+        rewrite E in Hr1_mult.
+        lia.
+      + exfalso. rewrite H2, Halign, multiplicity_countA in Hr1_mult by assumption.
+        fold ps in Hr1_mult.
+        rewrite E in Hr1_mult.
+        lia. } 
     destruct Hlr_bounds as [[Hl1 Hl2] [Hr1 Hr2]]. 
     apply le_INR in Hl1. apply lt_INR in Hl2. apply le_INR in Hr1. apply lt_INR in Hr2. 
-    cbn [INR] in Hl1, Hr1. foldR2. unfold Rabs. destruct_match ; lra.
+    cbn [INR] in Hl1, Hr1. foldR2. unfold Rabs. destruct_match.  ; lra.
   - pose (L' := line_calc (pos_list c)). fold L'.
     assert (H_LL' := @line_endpoints_invariant _ _ _ _ _ L L' (pos_list c)).
     feed_n 3 H_LL'.
@@ -3579,6 +3668,7 @@ apply Nat.le_lteq in Hr1_multR. case Hr1_multR as [Hr1_multR | Hr1_multR].
 Qed.
 
 Lemma phase3_transitions c da L w1 w2 : 
+  line_dir L <> 0%VS ->
   similarity_da_prop da ->
   inv3 c L w1 w2 -> 
   (exists w, inv1 (round gatherW da c) w) \/ 
diff --git a/CaseStudies/Gathering/InR2/Weber/Line.v b/CaseStudies/Gathering/InR2/Weber/Line.v
index f19784f8..db0f244b 100644
--- a/CaseStudies/Gathering/InR2/Weber/Line.v
+++ b/CaseStudies/Gathering/InR2/Weber/Line.v
@@ -263,6 +263,16 @@ case (Sumbool.sumbool_of_bool (forallb (fun x => L^-P (L^P x) ==b x) ps)).
   intros Halign. apply Hx, Halign, In_InA ; autoclass.
 Qed.
 
+Lemma aligned_on_InA_contains L ps t: InA equiv t ps -> aligned_on L ps -> line_contains L t.
+Proof.
+  intros Ht_InA Halign.
+  destruct (PermutationA_split setoid_equiv Ht_InA) as [ t' ht'].
+  rewrite ht' in Halign.
+  apply aligned_on_cons_iff in Halign.
+  destruct Halign as [Halign1 Halign2].
+  assumption.
+Qed.
+
 Definition aligned ps := exists L, aligned_on L ps.
 
 (* [aligned] doesn't depent on the order of the points. *)
@@ -975,6 +985,56 @@ Proof.
 Qed.
 
 
+Lemma line_on_inclA_ps L a ps1 ps2 : inclA equiv ps1 ps2 -> inclA equiv ((L ^on) a ps1) ((L ^on) a ps2).
+Proof.
+  intros h_incl.
+  unfold inclA , line_on.
+  intros x0 h_InA. 
+  rewrite filter_InA in h_InA;try typeclasses eauto.
+  rewrite filter_InA;try typeclasses eauto.
+  destruct h_InA as [h_InA h_eq].
+  split.
+  - now apply h_incl.
+  - assumption.  
+Qed.
+
+Lemma line_left_inclA_ps L a ps1 ps2 : inclA equiv ps1 ps2 -> inclA equiv ((L ^left) a ps1) ((L ^left) a ps2).
+Proof.
+  intros h_incl.
+  unfold inclA , line_left.
+  intros x0 h_InA. 
+  rewrite filter_InA in h_InA.
+  2:{ repeat red.
+      intros x1 y heq.
+      now rewrite heq. }
+  rewrite filter_InA.
+  2:{ repeat red.
+      intros x1 y heq.
+      now rewrite heq. }
+  destruct h_InA as [h_InA h_eq].
+  split.
+  - now apply h_incl.
+  - assumption.  
+Qed.
+
+Lemma line_right_inclA_ps L a ps1 ps2 : inclA equiv ps1 ps2 -> inclA equiv ((L ^right) a ps1) ((L ^right) a ps2).
+Proof.
+  intros h_incl.
+  unfold inclA , line_right.
+  intros x0 h_InA. 
+  rewrite filter_InA in h_InA.
+  2:{ repeat red.
+      intros x1 y heq.
+      now rewrite heq. }
+  rewrite filter_InA.
+  2:{ repeat red.
+      intros x1 y heq.
+      now rewrite heq. }
+  destruct h_InA as [h_InA h_eq].
+  split.
+  - now apply h_incl.
+  - assumption.  
+Qed.
 
 Lemma line_left_spec L x y ps : 
   InA equiv y (L^left x ps) <-> (InA equiv y ps /\ (L^P y < L^P x)%R).
@@ -986,6 +1046,22 @@ Lemma line_right_spec L x y ps :
   InA equiv y (L^right x ps) <-> (InA equiv y ps /\ (L^P y > L^P x)%R).
 Proof. unfold line_right. now rewrite filter_InA, Rltb_true ; [|intros ? ? ->]. Qed.
 
+Lemma line_left_diff L a ps:
+    ((L ^left) a ps) <> nil ->
+    aligned_on L ps ->
+    (L ^-P) ((L ^max) ((L ^left) a ps)) <> a.
+Proof.
+  intros h_left h_align.
+  intro abs.
+  assert (aligned_on L ((L ^left) a ps)) as h_align'.
+  { eapply aligned_on_inclA with ps;auto.
+    apply line_left_inclA. }
+  specialize (line_iP_max_InA L _ h_left h_align') as h.
+  rewrite abs in h.
+  rewrite line_left_spec in h.
+  lra.
+Qed.
+
 Lemma line_left_on_right_partition L x ps : 
   PermutationA equiv ps (L^left x ps ++ L^on x ps ++ L^right x ps).
 Proof.
@@ -1090,6 +1166,17 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma bipartition_max: forall L ps,
+    PermutationA equiv ps
+      ((L ^left) (L^-P (L^max ps)) ps ++(L ^on) (L^-P (L^max ps)) ps).
+Proof.
+  intros L ps. 
+  rewrite line_left_on_right_partition with (L:=L) (x:=(L^-P (L ^max ps))) at 1.
+  rewrite line_right_iP_max.
+  rewrite app_nil_r.
+  reflexivity.
+Qed.
+
 Lemma aggravate_right: forall L ps w w',
     ((L^P w) < (L^P w'))%R
     -> L^right w' ps = L^right w' (L^right w ps).
@@ -1103,7 +1190,20 @@ Proof.
   etransitivity;eauto.
 Qed.
 
-Lemma aggravate_on: forall L ps w w',
+Lemma aggravate_left: forall L ps w w',
+    ((L^P w') < (L^P w))%R
+    -> L^left w' ps = L^left w' (L^left w ps).
+Proof.
+  symmetry.
+  unfold line_left.
+  rewrite filter_comm.
+  rewrite filter_weakened;auto.
+  intros x H1 H2. 
+  rewrite  Rltb_true in *|- *.
+  etransitivity;eauto.
+Qed.
+
+Lemma aggravate_on_right: forall L ps w w',
     ((L^P w) < (L^P w'))%R
     -> L^on w' ps = L^on w' (L^right w ps).
 Proof.
@@ -1120,6 +1220,103 @@ Proof.
   now rewrite <- heq.
 Qed.
 
+Lemma aggravate_on_left: forall L ps w w',
+    ((L^P w') < (L^P w))%R
+    -> L^on w' ps = L^on w' (L^left w ps).
+Proof.
+  intros L ps w' w H0. 
+  unfold line_on, line_left.
+  rewrite <- filter_andb.
+  apply filter_extensionality_compat;auto.
+  repeat intro.
+  subst y.
+  destruct ((L ^P) w ==b (L ^P) x) eqn:heq;cbn;auto;[].
+  symmetry.
+  rewrite eqb_true_iff in heq.
+  rewrite Rltb_true.
+  now rewrite <- heq.
+Qed.
+
+Theorem PermutationA_app_inv_l : forall {A : Type} [eqA : relation A],
+    Equivalence eqA ->
+    forall(l l1 l2:list A),
+    PermutationA eqA (l ++ l1) (l ++ l2) ->
+    PermutationA eqA l1 l2.
+Proof.
+  induction l; simpl; auto.
+  intros.
+  apply IHl.
+  apply PermutationA_cons_inv with a; auto.
+Qed.
+
+Theorem PermutationA_app_inv_r : forall {A : Type} [eqA : relation A],
+    Equivalence eqA ->
+    forall(l l1 l2:list A),
+      PermutationA eqA (l1 ++ l) (l2 ++ l) ->
+      PermutationA eqA l1 l2.
+Proof.
+  intros A eqA H0 l l1 l2 h.
+  rewrite 2 (PermutationA_app_comm _ _ l) in h.
+  eapply PermutationA_app_inv_l ;try typeclasses eauto.
+  eassumption.
+Qed.
+
+Lemma aggravate_right': forall L ps w w',
+    ((L^P w') < (L^P w))%R
+    -> L^right w' (L^left w ps) = nil
+    -> L^on w ps = nil
+    -> PermutationA equiv (L^right w' ps) (L^right w ps).
+Proof.
+  intros L ps w w' H0 H1 H2. 
+  specialize (line_left_on_right_partition L w' ps) as h1.
+  specialize (line_left_on_right_partition L w ps) as h2.
+  rewrite H2 in h2.
+  rewrite app_nil_l in h2.
+  assert (PermutationA equiv ((L ^left) w' ps ++ (L ^on) w' ps) ((L ^left) w ps)).
+  { specialize (line_left_on_right_partition L w' ((L ^left) w ps)) as h3.
+    rewrite H1 in h3.
+    rewrite app_nil_r in h3.
+    rewrite <- aggravate_left in h3;auto.
+    rewrite <- aggravate_on_left in h3;auto.
+    rewrite h3.
+    reflexivity. }
+  rewrite <- H3 in h2.
+  rewrite app_assoc in h1.
+  rewrite h1 in h2 at 1.
+  apply PermutationA_app_inv_l with (2:=h2).
+  typeclasses eauto.
+Qed.
+(*
+Lemma aggravate_left': forall L ps w w',
+    ((L^P w') < (L^P w))%R
+    -> L^right w' (L^left w ps) = nil
+    -> L^on w' ps = nil
+    -> PermutationA equiv (L^left w ps) (L^left w' ps).
+Proof.
+  intros L ps w w' H0 H1 H2.
+  specialize (line_left_on_right_partition L w' ps) as h1.
+  specialize (line_left_on_right_partition L w ps) as h2.
+  rewrite H2 in h1.
+  rewrite app_nil_l in h1.
+  assert (PermutationA equiv ((L ^right) w ps ++ (L ^on) w ps) ((L ^right) w' ps)).
+  { specialize (line_left_on_right_partition L w ((L ^right) w' ps)) as h3.
+    rewrite H2 in h3.
+    rewrite app_nil_r in h3.
+    rewrite <- aggravate_left in h3;auto.
+    rewrite <- aggravate_on_left in h3;auto.
+    rewrite h3.
+    reflexivity.
+  }
+  rewrite <- H3 in h2.
+  rewrite app_assoc in h1.
+  rewrite h1 in h2 at 1.
+  symmetry.
+  apply PermutationA_app_inv_l with (2:=h2).
+  typeclasses eauto.
+Qed.
+*)
+
+
 Lemma line_on_length_aligned L x ps : 
   aligned_on L (x :: ps) ->
   length (L^on x ps) = countA_occ equiv EQ0 x ps.
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index 116accba..230b4916 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -1760,6 +1760,20 @@ rewrite <-(line_on_length_aligned L _ _ Halign).
 f_equiv. rewrite <-Rabs_Ropp. f_equiv. lra.
 Qed.
 
+(* A variant for the left to right part with a different hypothesis. *)
+Lemma weber_aligned_spec_weak_right L ps w : 
+  line_dir L =/= 0%VS ->
+  ps <> nil ->
+  aligned_on L ps -> 
+  Weber ps w -> 
+  (Rabs (INR (length (L^left w ps)) - INR (length (L^right w ps))) <= INR (length (L^on w ps)))%R.
+Proof. 
+intros Hdir Halign' Hnonnil HWeber. 
+apply weber_aligned_spec_weak;auto.
+apply aligned_on_cons_iff;split;auto.
+eapply weber_aligned;eauto.
+Qed.
+
 Lemma line_on_app: forall (L: line) (l l':list R2) x,
     PermutationA equiv ((L ^on) x (l++l')) (((L ^on) x l) ++ ((L ^on) x l')) .
 Proof.
@@ -2200,7 +2214,7 @@ Proof.
     rewrite line_P_iP_min in h_InA.            
     apply h_InA. }
   rewrite <- aggravate_right in h;auto.
-  rewrite <- aggravate_on in h;auto.
+  rewrite <- aggravate_on_right in h;auto.
   rewrite <- h in h_w.
   apply (f_equal INR) in h, h_w.
   rewrite plus_INR in h,h_w.
@@ -2266,7 +2280,7 @@ Qed.
    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 : 
+Lemma weber_aligned_spec_right_bigger L ps w : 
   ps <> nil ->                  (* Seems necessary *)
   line_dir L =/= 0%VS ->
   aligned_on L (w :: ps) -> 
@@ -2287,7 +2301,7 @@ Proof.
       assumption.
 Qed.
 
-Lemma weber_aligned_spec_left L ps w : 
+Lemma weber_aligned_spec_left_bigger L ps w : 
   ps <> nil ->                  (* Seems necessary *)
   line_dir L =/= 0%VS ->
   aligned_on L (w :: ps) -> 
@@ -2318,17 +2332,466 @@ Proof.
 Qed.
 
 
+Lemma INR_length_0: forall A (l:list A) , (INR (length l)) = 0%R -> l = nil.
+Proof.
+  intros A l H. 
+  destruct (Nat.eq_decidable (length l) 0).
+  - now apply length_0.
+  - assert (0 < Rlength l).
+    { lia. }
+    apply (lt_0_INR (length l)) in H1.
+    exfalso.
+    lra.
+Qed.
+
+Lemma weber_aligned_spec_on 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 -> 
+  (0 < ^R (L^on w ps))%R.
+Proof.
+  intros h_neq_ps_nil h_nequiv_line_dir_origin h_align_L_cons h_eq_Rminus_ h_OnlyWeber_ps_w_.
+  destruct (Rlt_dec 0 (^R (L ^on) w ps)%R) as [h|h];auto.
+  exfalso.
+  assert (aligned_on L ps) as h_align_ps.
+  { apply aligned_on_cons_iff in h_align_L_cons.
+    apply h_align_L_cons. }
+  assert (((^R (L ^on) w ps) = 0)%R) as h_w_not_occupied.
+  { assert (0 <= (^R (L ^on) w ps))%R.
+    { apply pos_INR. }
+    lra. }
+  remember ((L ^-P) ((L ^max) ((L ^left) w ps))) as w'.
+  assert ((L ^left) w ps <> nil) as h_left_w_nonnil.
+  { specialize (line_left_on_right_partition L w ps) as h_tri.
+    apply PermutationA_length in h_tri.
+    repeat rewrite app_length in h_tri. 
+    apply (f_equal INR) in h_tri.
+    repeat rewrite plus_INR in h_tri.
+    intro abs. 
+    apply (f_equal (@length R2)) in abs.
+    apply (f_equal INR) in abs.
+    cbn [length INR] in abs.
+    rewrite abs in h_tri.
+    assert ((^R ps) > 0)%R.
+    { apply lt_0_INR.
+      apply Nat.neq_0_lt_0.
+      intro abs2.
+      apply length_zero_iff_nil in abs2.
+      contradiction. }
+    lra. }
+  assert (Weber ps w') as h_weber_w'.
+  { assert (aligned_on L (w' :: ps)) as h_align_w'.
+    { apply aligned_on_cons_iff.
+      split;auto.
+      subst w'.
+      apply line_contains_proj_inv;auto. }
+    assert (((L ^P) w' < (L ^P) w)%R) as h_lt_on_w_w'.
+    { destruct (line_left_spec L w w' ps) as [ h_left1 h_left2 ].
+        apply h_left1.
+        rewrite Heqw'.
+        apply line_iP_max_InA;auto.
+        apply aligned_on_inclA with (ps':=ps).
+        - apply line_left_inclA.
+        - now apply (aligned_on_cons_iff L w). }
+    apply (@weber_aligned_spec_weak L ps w');auto.
+    specialize (bipartition_max L ((L^left) w ps)) as h''.
+    rewrite <- Heqw' in h''.
+    rewrite <- aggravate_left in h'';auto.
+    assert (PermutationA equiv
+              ((L ^on) w' ((L ^left) w ps))
+              ((L ^on) w' ps))%R as h_simpl_on.
+    { rewrite <- aggravate_on_left;auto.
+      reflexivity. }
+    rewrite h_simpl_on in h''.
+    assert (PermutationA equiv ((L ^right) w' ps) ((L ^right) w ps))%R as h_right_same.
+    { assert (PermutationA equiv ((L ^right) w' ps) ((L ^right) w ps)) as h_right_w_w'.
+      { apply aggravate_right';auto.
+        - rewrite Heqw'.
+          rewrite line_right_iP_max;auto.
+        - now apply INR_length_0. }
+      rewrite h_right_w_w'.
+      reflexivity. }
+    assert ((^R (L ^on) w' ps) > 0)%R.
+    { specialize (line_iP_max_InA L ((L ^left) w ps) h_left_w_nonnil) as h_max.
+      rewrite <- Heqw' in h_max.
+      assert(aligned_on L ((L ^left) w ps)).
+      { apply aligned_on_inclA with ps; auto.
+        now apply line_left_inclA. }
+      specialize h_max with (1:=H).
+      assert(((L ^P) w') == ((L ^P) w')) as h_tmp by reflexivity.
+      pose (conj h_max h_tmp).
+      clearbody a.
+      
+      rewrite <- line_on_spec in a.
+      assert(InA equiv w' ((L ^on) w' ps)).
+      { assert (inclA equiv ((L ^on) w' ((L ^left) w ps)) ((L ^on) w' ps)) as h_incl.
+        { apply line_on_inclA_ps.
+          apply line_left_inclA. }
+        now apply h_incl. }
+      apply (@InA_nth _ equiv 0%VS w' ((L ^on) w' ps)) in H0.
+      destruct H0 as [n [y [h1 h2]]].
+      assert (0 < Rlength ((L ^on) w' ps)) by lia.
+      apply lt_INR in H0.
+      cbn in H0.
+      lra. }
+    assert ((^R (L ^left) w' ps) < (^R (L ^right) w' ps))%R as h_left_less.
+    { apply PermutationA_length in h_right_same.
+      rewrite h_right_same.
+      assert ((^R (L ^right) w ps) = (^R (L ^left) w ps))%R as h_eq_ww'.
+      { lra. }
+      rewrite h_eq_ww'.
+      rewrite h''.
+      rewrite app_length,plus_INR.
+      lra. }
+    apply Req_le.
+    rewrite <- h_right_same in h_eq_Rminus_.
+    rewrite h'' in h_eq_Rminus_.
+    rewrite app_length in h_eq_Rminus_. 
+    rewrite plus_INR in h_eq_Rminus_.
+    rewrite Rabs_left1;
+    lra. }
+  assert (w =/= w') as h_neq.
+  { intro abs.
+    destruct ((L ^left) w ps) eqn:heq.
+    { now destruct h_left_w_nonnil. }
+    apply (line_left_diff L w ps);auto.
+    - rewrite heq.
+      auto.
+    - now rewrite heq, <- Heqw'. }
+  destruct h_OnlyWeber_ps_w_ as [hweb hwebeq].
+  apply h_neq.
+  symmetry.
+  eapply hwebeq;eauto.
+Qed.
+
+Require Import LibHyps.LibHyps.
+Lemma right_lt: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} {H : EuclideanSpace T} 
+                       (L : line) (ps : list T) (w w' : T), 
+    ((L ^P) w' < (L ^P) w)%R ->
+    ((^R (L ^right) w' ps) >= (^R (L ^right) w ps) + (^R (L ^on) w ps))%R.
+Proof.
+  intros T S0 EQ0 VS ES L ps w w' h_lt. 
+  specialize (line_left_on_right_partition L w ps) as h.
+  assert (PermutationA equiv ((L ^right) w' ps) ((L ^right) w' ((L ^left) w ps ++ (L ^on) w ps ++ (L ^right) w ps)))
+    as heq.
+  { unfold line_right at 1 2.
+    apply filter_PermutationA_compat;auto.
+    typeclasses eauto. }
+  unfold line_right at 2 in heq.
+  repeat rewrite filter_app in heq.
+  change (filter (fun y : T => Rltb ((L ^P) w') ((L ^P) y)) ((L ^on) w ps))
+    with ((L ^right) w' ((L ^on) w ps))
+    in heq.
+  change (filter (fun y : T => Rltb ((L ^P) w') ((L ^P) y)) ((L ^right) w ps))
+    with ((L ^right) w' ((L ^right) w ps))
+    in heq.
+  assert (PermutationA equiv ((L ^right) w' ((L ^right) w ps)) ((L ^right) w ((L ^right) w' ps))) as h_perm_right.
+  { unfold line_right. 
+    rewrite filter_comm.
+    reflexivity. }
+  rewrite h_perm_right in heq.
+  rewrite <- aggravate_right in heq;auto.
+  assert (PermutationA equiv ((L ^right) w' ((L ^on) w ps)) ((L ^on) w ps)) as h_on_right.
+  { unfold line_right, line_on.
+    rewrite filter_weakenedA;auto.
+    - reflexivity.
+    -  intros x h1 h2.
+       rewrite Rltb_true.
+       rewrite eqb_true_iff in h2.
+       rewrite <- h2.
+       assumption. }
+  rewrite h_on_right in heq.
+  rewrite heq.
+  repeat rewrite app_length.
+  repeat rewrite plus_INR.
+  match goal with |- (?A + _ >= _)%R => remember A as hh
+  end.
+  assert (hh >= 0)%R.
+  { rewrite Heqhh.
+    apply Rle_ge.
+    apply pos_INR. }
+  lra.
+Qed.
+
+Lemma left_lt: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} {H : EuclideanSpace T} 
+                       (L : line) (ps : list T) (w w' : T), 
+    ((L ^P) w < (L ^P) w')%R ->
+    ((^R (L ^left) w' ps) >= (^R (L ^left) w ps) + (^R (L ^on) w ps))%R.
+Proof.
+  intros T S0 EQ0 VS ES L ps w w' h_lt. 
+  specialize (line_left_on_right_partition L w ps) as h.
+  assert (PermutationA equiv ((L ^left) w' ps) ((L ^left) w' ((L ^left) w ps ++ (L ^on) w ps ++ (L ^right) w ps)))
+    as heq.
+  { unfold line_left at 1 2.
+    apply filter_PermutationA_compat;auto.
+    repeat red.
+    intros x y heqxy. 
+    now rewrite heqxy. }
+  unfold line_left at 2 in heq.
+  repeat rewrite filter_app in heq.
+  change (filter (fun y : T => Rltb ((L ^P) y) ((L ^P) w')) ((L ^on) w ps))
+    with ((L ^left) w' ((L ^on) w ps))
+    in heq.
+  change (filter (fun y : T => Rltb ((L ^P) y) ((L ^P) w')) ((L ^left) w ps))
+    with ((L ^left) w' ((L ^left) w ps))
+    in heq.
+  assert (PermutationA equiv ((L ^left) w' ((L ^left) w ps)) ((L ^left) w ((L ^left) w' ps))) as h_perm_left.
+  { unfold line_left.
+    rewrite filter_comm.
+    reflexivity. }
+  rewrite h_perm_left in heq.
+  rewrite <- aggravate_left in heq;auto.
+  assert (PermutationA equiv ((L ^left) w' ((L ^on) w ps)) ((L ^on) w ps)) as h_on_left.
+  { unfold line_left, line_on.
+    rewrite filter_weakenedA;auto.
+    - reflexivity.
+    -  intros x h1 h2.
+       rewrite Rltb_true.
+       rewrite eqb_true_iff in h2.
+       rewrite <- h2.
+       assumption. }
+  rewrite h_on_left in heq.
+  rewrite heq.
+  repeat rewrite app_length.
+  repeat rewrite plus_INR.
+  match goal with |- (_ + (_+?A) >= _)%R => remember A as hh
+  end.
+  assert (hh >= 0)%R.
+  { rewrite Heqhh.
+    apply Rle_ge.
+    apply pos_INR. }
+  lra.
+Qed.
+
+Lemma left_weaker: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} {H : EuclideanSpace T} 
+                          (L : line) (ps : list T) (w w' : T), 
+    ((L ^P) w' < (L ^P) w)%R -> 
+    ((^R (L ^left) w' ps) <= (^R (L ^left) w ps))%R.
+Proof.
+  intros T S0 EQ0 VS ES L ps w w' h_Rlt_line_proj.
+  unfold line_left.
+  rewrite <- (filter_weakenedA (fun y => Rltb ((L ^P) y) ((L ^P) w')) (fun y => Rltb ((L ^P) y) ((L ^P) w))).
+  - rewrite filter_comm.
+    apply le_INR.
+    rewrite filter_length at 1.
+    lia.
+  - intros x0 H0 H1.
+    rewrite Rltb_true in H1 |- *.
+    lra.
+Qed.
+
+Lemma right_weaker: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} {H : EuclideanSpace T} 
+                           (L : line) (ps : list T) (w w' : T), 
+    ((L ^P) w < (L ^P) w')%R -> 
+    ((^R (L ^right) w' ps) <= (^R (L ^right) w ps))%R.
+Proof.
+  intros T S0 EQ0 VS ES L ps w w' h_Rlt_line_proj.
+  unfold line_right.
+  rewrite <- (filter_weakenedA (fun y => Rltb ((L ^P) w') ((L ^P) y)) (fun y => Rltb ((L ^P) w) ((L ^P) y))).
+  - rewrite filter_comm.
+    apply le_INR.
+    rewrite filter_length at 1.
+    lia.
+  - intros x0 H0 H1.
+    rewrite Rltb_true in H1 |- *.
+    lra.
+Qed.
 
 
+Lemma weber_aligned_spec_right_bigger_2 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 ->
+  (Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R ->
+  OnlyWeber ps w.
+Proof. 
+  intros h_neq_ps_nil h_line_dir h_align h_left_right h_Rlt_Rabs.
+  (* assert ( ((^R (L ^left) w ps) - (^R (L ^right) w ps) + 1 <= 0)%R) as h_left_right'. *)
+  (* { admit. } *)
+  specialize (weber_aligned_spec_weak h_line_dir h_align) as h_weak.
+  apply Rlt_le in h_Rlt_Rabs as h_Rle_Rabs.
+  apply <- h_weak in h_Rle_Rabs.
+  clear h_weak.
+  split;auto.
+  intros x h_weber.
+  destruct (equiv_dec x w);auto.
+  exfalso.
+  apply aligned_on_cons_iff in h_align as h.
+  destruct h as [h_line h_align_ps].
+  assert (aligned_on L (x::ps)) as h_align_ps'.
+  { apply aligned_on_cons_iff.
+    split;auto.
+    eapply weber_aligned;eauto. }
+  specialize (weber_aligned h_neq_ps_nil h_align_ps h_weber) as h_align_x.
+  specialize (weber_aligned_spec_weak_right h_line_dir h_neq_ps_nil h_align_ps h_weber) as h_rabs.
+  apply Rabs_left in h_left_right as hrabs_eq.
+  rewrite hrabs_eq in *.
+  clear hrabs_eq.
+  rewrite Ropp_minus_distr' in h_Rlt_Rabs.
+  remember (^R (L ^left) x ps) as leftx in *.
+  remember (^R (L ^right) x ps) as rightx in *.
+  remember (^R (L ^on) x ps) as onx in *.
+  remember (^R (L ^left) w ps) as leftw in *.
+  remember (^R (L ^right) w ps) as rightw in *.
+  remember (^R (L ^on) w ps) as onw in *.
+
+  assert (onx+leftx+rightx = onw+leftw+rightw)%R as h_eq_partition.
+  { specialize (line_left_on_right_partition L x ps) as h1.
+    specialize (line_left_on_right_partition L w ps) as h2.
+    rewrite h1 in h2 at 1.
+    apply PermutationA_length in h2.
+    apply (f_equal INR) in h2.
+    repeat rewrite app_length in h2.
+    repeat rewrite plus_INR in h2.
+    
+    rewrite <- Heqrightx,<- Heqleftx, <- Heqleftw, <-Heqrightw, <- Heqonx, <- Heqonw in h2.
+    lra. }
+
+  assert (L^P x <> L^P w) as h_proj.
+  { intro abs.
+    apply (f_equal (line_proj_inv L)) in abs.
+    rewrite <- h_line in c.
+    rewrite <- h_align_x in c.
+    contradiction. }
+  specialize (Rdichotomy _ _ h_proj) as [h_proj' | h_proj'].
+  - assert (rightx >= rightw + onw )%R.
+    { rewrite Heqrightx , Heqonw , Heqrightw.
+      now apply right_lt. }
+    assert (onx + leftx <= leftw)%R.
+    { lra. }
+    clear H0.
+    assert (onx >= 0)%R.
+    { rewrite Heqonx.
+      apply Rle_ge.
+      apply pos_INR. }
+    assert ((rightx - leftx) <= onx)%R.
+    { rewrite Rabs_left1 in h_rabs.
+      - lra.
+      - lra. }
+    clear c.
+    clear h_proj'.
+    clear h_proj.
+    lra.
+
+  -  /g.
+     assert (onw > 0)%R by lra.
+     assert (leftx >= leftw + onw )%R.
+    { rewrite Heqleftx, Heqleftw, Heqonw.
+      now apply left_lt. }
+    assert (rightx <= rightw)%R.
+    { rewrite Heqrightx, Heqrightw.
+      now apply right_weaker. }
+     assert (leftx > rightx)%R by lra.
+     assert (leftx - rightx <= onx)%R.
+     { rewrite  Rabs_pos_eq in h_rabs;lra. }
+     clear h_rabs.
+     
+    assert (onw >=0)%R.
+    { rewrite Heqonw.
+      apply Rle_ge.
+      apply pos_INR. }
+    assert (onx >=0)%R.
+    { rewrite Heqonx.
+      apply Rle_ge.
+      apply pos_INR. }
+    assert (leftw >=0)%R.
+    { rewrite Heqleftw.
+      apply Rle_ge.
+      apply pos_INR. }
+    assert (leftx >=0)%R.
+    { rewrite Heqleftx.
+      apply Rle_ge.
+      apply pos_INR. }
+    assert (rightw >=0)%R.
+    { rewrite Heqrightw.
+      apply Rle_ge.
+      apply pos_INR. }
+    assert (rightx >=0)%R.
+    { rewrite Heqrightx.
+      apply Rle_ge.
+      apply pos_INR. }
+    clear h_proj.
+    assert (rightx + onx <= rightw)%R by lra.
+
+    assert (rightw - leftw + 1 <= onw)%R.
+    { (* hideously going back and forth from R to nat. *)
+      rewrite Heqrightw, Heqleftw, Heqonw.
+      rewrite <- minus_INR.
+      2:lra.
+      change (IZR (Zpos xH)) with (INR 1).
+      rewrite <- plus_INR.
+      apply le_INR.
+      apply not_gt.
+      intro abs.
+      apply le_INR in abs.
+      change (S (Rlength ((L ^on) w ps)))
+        with (1+(Rlength ((L ^on) w ps))) in abs.
+      repeat rewrite  plus_INR in abs.
+      rewrite minus_INR in abs.
+      2: lra.
+      change (INR 1) with (IZR (Zpos xH)) in abs.
+      rewrite  <- Heqrightw, <- Heqleftw, <- Heqonw in abs.
+      lra. }
+    
+    clear h_left_right.
+    clear h_Rlt_Rabs.
+    lra.
+Qed.
+
+Lemma weber_aligned_spec_left_bigger_2 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 ->
+  (Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R ->
+  OnlyWeber ps w.
+Proof. 
+Admitted.
+Lemma weber_aligned_spec_on_2 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 ->
+  (0 < ^R (L^on w ps))%R ->
+  OnlyWeber ps w.
+Proof.
+Admitted.
+
 Lemma weber_aligned_spec L ps w : 
   ps <> nil ->                  (* Seems necessary *)
   line_dir L =/= 0%VS ->
   aligned_on L (w :: ps) -> 
-    OnlyWeber ps w -> 
-    (Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R.
+  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. 
+Proof.
   intros Hpsnonnil Hlinedir Halign. 
+  split.
+  { intro HonlyWeber.
+    destruct ((Req_appart_dec ((^R (L^right w ps)) - (^R (L^left w ps))) 0)%R) as [ | [| ]].
+    - rewrite Rabs_right;try lra.
+      assert ((^R (L ^left) w ps) - (^R (L ^right) w ps) = 0)%R as heq.
+      { lra. }
+      rewrite heq.
+      apply weber_aligned_spec_on;auto.
+    - apply weber_aligned_spec_left_bigger;auto.
+    - apply weber_aligned_spec_right_bigger;auto.
+      lra. }
+  { intro Hlt.
+    destruct ((Req_appart_dec ((^R (L^right w ps)) - (^R (L^left w ps))) 0)%R) as [ | [| ]].
+    - apply weber_aligned_spec_on_2 with L;auto.
+      assert (((^R (L ^left) w ps) - (^R (L ^right) w ps))%R = 0%R) by lra.
+      rewrite H,Rabs_R0 in Hlt.
+      assumption.
+    - apply weber_aligned_spec_left_bigger_2 with L;auto.
+    - apply weber_aligned_spec_right_bigger_2 with L;auto.
+      lra. }
+Qed.
+
+(*
   specialize (weber_aligned_spec_weak Hlinedir Halign) as h_weak. 
   destruct
     (Rcase_abs ((^R (L ^left) w ps)
@@ -2705,7 +3168,7 @@ line_left_on_right_partition
   - admit.
 
 Qed.
-
+*)
 Lemma weber_majority ps w : 
   countA_occ equiv R2_EqDec w ps > (Nat.div2 (length ps + 1)) -> OnlyWeber ps w. 
 Proof. Admitted.  
-- 
GitLab