diff --git a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
index 441f51983cc2bd11b33db712b02322606a2f43c8..6c16f6de8d4a3c9fa08f8f81dfe8f500c856ee6e 100644
--- a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
+++ b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
@@ -555,7 +555,6 @@ Proof using Type.
     reflexivity.
 Qed.
 
-
 Lemma find_map {A B} (f : B -> bool) (g : A -> B) (l : list A) : 
   find f (List.map g l) = option_map g (find (fun x => f (g x)) l).
 Proof using Type.
@@ -1889,7 +1888,7 @@ Proof using lt_0n.
   foldR2.
   rewrite <- h_equiv_robot_with_mult_robot_with_mult_.
   destruct (robot_with_mult (Nat.div2 (cardinal x + 1)) (multi_support x))
-    as [l | h_eq_robot_with_mult_None_] eqn:h_eq_robot_with_mult_l_  .
+    as [l | ] eqn:h_eq_robot_with_mult_l_  .
   { cbn -[multi_support].
     now rewrite hsupp. }
   remember (line_calc (multi_support x)) as Lx.
@@ -2245,22 +2244,72 @@ 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 ( invalid_obs obs -> invalid_obs (obs_from_config config (config (Good g)))) as h_valid_sim.
+{ fold sim in f,f_inv.
+  intro abs.
+  unfold obs in abs.
+  unfold f in abs.
+  rewrite <- obs_from_config_map in abs.
+
+  red in abs|-*.
+  destruct abs as [x [y [hneq_xy [heq_card [h_multx h_multy]]]]].
+  exists (sim ⁻¹ x), (sim ⁻¹ y).
+  repeat split.
+  * intro abs.
+    apply hneq_xy.
+    apply (Bijection.injective (sim ⁻¹)).
+    assumption.
+  * rewrite n_cardinal.
+    lia.
+  * rewrite n_cardinal.
+    assert (x == (sim (sim ⁻¹ x))) as h_eq'.
+    { rewrite (Bijection.section_retraction sim x).
+      auto. }
+    rewrite h_eq' in h_multx.
+    rewrite map_injective_spec in h_multx;try typeclasses eauto.
+    -- rewrite h_multx.
+       rewrite map_cardinal;try typeclasses eauto.
+       rewrite n_cardinal.
+       reflexivity.
+    -- apply injective.
+  * rewrite n_cardinal.
+    assert (y == (sim (sim ⁻¹ y))) as h_eq'.
+    { rewrite (Bijection.section_retraction sim y).
+      auto. }
+    rewrite h_eq' in h_multy.
+    rewrite map_injective_spec in h_multy;try typeclasses eauto.
+    -- rewrite h_multy.
+       rewrite map_cardinal;try typeclasses eauto.
+       rewrite n_cardinal.
+       reflexivity.
+    -- apply injective.
+  * apply f_compat. }
+
 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].
-  + symmetry. apply robot_with_mult_unique ; auto.
-    change obs with (!! (map_config (lift f) config)).
-    rewrite multi_support_map by auto. rewrite map_map.
-    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. *)
-}
+{ rewrite robot_with_mult_map;try typeclasses eauto.
+  - setoid_rewrite <-(n_cardinal config (config (Good g))).
+    rewrite (@robot_with_mult_unique_obs obs (List.map sim (pos_list config)));auto.
+    + unfold obs.
+      repeat rewrite cardinal_obs_from_config.
+      reflexivity.
+    + clear L L' r1 r2 r1' r2' Hmiddle.
+      clear Hw_perm w2' w1' Hw w2 w1.
+      fold sim in f,f_inv.
+      rewrite (invalid_config_obs config (config (Good g))) in Hvalid.
+      intro abs.
+      apply Hvalid.
+      now apply h_valid_sim.
+    + unfold obs, sim.
+      specialize (multi_support_map f config) as h.
+      unfold f in h at 3.
+      cbn [projT1] in h.
+      rewrite h;try typeclasses eauto.
+      reflexivity.
+  - unfold sim.
+    apply Bijection.injective. }
 
 assert (Hcenter : 0%VS == sim (get_location (config (Good g)))).
+
 { rewrite <-Hsim. cbn. unfold sim. now rewrite Bijection.section_retraction. }
 
 assert (Hseg : forall t, existsb (strict_segment_decb 0%VS (sim t)) (multi_support obs) =
@@ -2293,9 +2342,15 @@ assert (Hweb_align : w1 =/= w2 -> aligned (pos_list config)).
 
 destruct (obs_invalid_dec obs) at 1.
 { exfalso.
-  admit. }
-destruct (length (multi_support obs)).
-{ admit. }
+  apply Hvalid.
+  setoid_rewrite -> (invalid_config_obs config (config (Good g))).
+  now apply h_valid_sim. }
+destruct (length (multi_support obs)) eqn:heq_supp.
+{ exfalso.
+  rewrite multi_set_length_cardinal in heq_supp.
+  unfold obs in heq_supp.
+  rewrite n_cardinal in heq_supp.
+  lia. }
 cbn [ equiv_dec nat_EqDec Nat.eq_dec nat_rec nat_rect].
 
 case Hw_perm as [[<- <-] | [<- <-]]. 
@@ -2303,7 +2358,8 @@ case Hw_perm as [[<- <-] | [<- <-]].
   - reflexivity.
   - exfalso. apply Hw'. now apply (Similarity.injective sim).
   - exfalso. apply Hw_sim. now f_equal.
-  - foldR2. 
+  - foldR2.
+
     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.
@@ -2337,7 +2393,7 @@ case Hw_perm as [[<- <-] | [<- <-]].
           rewrite <-segment_decb_false in Hm3. foldR2. rewrite Hm3.
           destruct_match ; reflexivity.
         --repeat destruct_match ; reflexivity.
-Admitted.
+Qed.
 
 (* This is the property : all robots are looping. 
  * This is what should be verified in the initial configuration. *)
@@ -2503,15 +2559,18 @@ destruct H as [w1 [w2 [Halign [Hweb NEw12]]]].
 apply NEw12.
 cut (L^P w1 == L^P w2).
 { intros HeqP. apply (f_equal (L^-P)) in HeqP. 
-  rewrite 2 Halign in HeqP by apply (weber_segment_InA Hweb). assumption. }
+  rewrite 2 Halign in HeqP.
+  - assumption.
+  - apply (weber_segment_InA (pos_list_non_nil _) NEw12 Hweb);auto.
+  - apply (weber_segment_InA (pos_list_non_nil _) NEw12 Hweb);auto. }
 assert (Hmin_max : L^max (pos_list c) == L^min (pos_list c)).
 { rewrite <-line_P_iP_min, <-line_P_iP_max. foldR2. now rewrite Er12. }
 transitivity (L^min (pos_list c)).
 + assert (Hbounds := line_bounds L (pos_list c) w1).
-  feed Hbounds. { apply (weber_segment_InA Hweb). }
+  feed Hbounds. { apply (weber_segment_InA (pos_list_non_nil _) NEw12 Hweb). }
   rewrite Hmin_max in Hbounds. now apply Rle_antisym.
 + assert (Hbounds := line_bounds L (pos_list c) w2).
-  feed Hbounds. { apply (weber_segment_InA Hweb). }
+  feed Hbounds. { apply (weber_segment_InA (pos_list_non_nil _) NEw12 Hweb). }
   rewrite Hmin_max in Hbounds. now apply Rle_antisym.
 Qed.
 
@@ -2731,7 +2790,7 @@ case (w1 =?= w2) as [Ew12 | NEw12].
   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. 
-    specialize (weber_segment_InA Hweb) as Hweb'. destruct Hweb' as [Hw1_InA Hw2_InA].
+    specialize (weber_segment_InA h_psnonnil NEw12 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).
@@ -2820,8 +2879,8 @@ case (w1 =?= w2) as [Ew12 | NEw12].
           ** repeat rewrite (line_middle L ps) in Hmiddle at 1.
              repeat rewrite line_P_iP in Hmiddle at 1 by assumption.
             fold ps. foldR2. case Hmiddle; lra.
-          **apply Halign, (weber_segment_InA Hweb).
-          **apply Halign, (weber_segment_InA Hweb).
+          **apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
+          **apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
           **apply line_contains_middle ; unfold line_contains ; [now rewrite line_P_iP_min | now rewrite line_P_iP_max].
       ++exists L, w2, w1. split ; [|split ; [|split ; [|split ; [|split ; [|split]]]]] ;
           auto using config_stay_impl_config_stg, config_stay_impl_endpoints_stay.
@@ -2831,8 +2890,8 @@ case (w1 =?= w2) as [Ew12 | NEw12].
           ** repeat rewrite (line_middle L ps) in Hmiddle at 1.
              repeat rewrite line_P_iP in Hmiddle at 1 by assumption.
             fold ps. foldR2. case Hmiddle ; lra.
-          **apply Halign, (weber_segment_InA Hweb).
-          **apply Halign, (weber_segment_InA Hweb).
+          **apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
+          **apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
           **apply line_contains_middle ; unfold line_contains ; [now rewrite line_P_iP_min | now rewrite line_P_iP_max].
     * (* Phase 4. *)
       right.
@@ -2841,15 +2900,15 @@ case (w1 =?= w2) as [Ew12 | NEw12].
         case (Rle_dec (L^P w1) (L^P w2)) as [[Hlt | Heq] | Hgt] ; [left | exfalso | right].
         + assumption.
         + apply NEw12. apply (f_equal (L^-P)) in Heq. 
-          rewrite 2 Halign in Heq by apply (weber_segment_InA Hweb). assumption.
+          rewrite 2 Halign in Heq by apply (weber_segment_InA h_psnonnil NEw12 Hweb). assumption.
         + lra.   
       }
       case Cw12 as [Cw12 | Cw12].
       ++assert (Hlr : ((L^min ps + L^max ps) / 2 < L^P w1 \/ L^P w2 < (L^min ps + L^max ps) / 2)%R).
         { rewrite (segment_line L) in Hmiddle.
           + rewrite line_middle in Hmiddle. rewrite line_P_iP in Hmiddle by assumption. lra.
-          + apply Halign, (weber_segment_InA Hweb).
-          + apply Halign, (weber_segment_InA Hweb).
+          + apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
+          + apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
           + apply line_contains_middle ; unfold line_contains ; [now rewrite line_P_iP_min | now rewrite line_P_iP_max]. }
         clear Hmiddle. case Hlr as [Hmiddle | Hmiddle].
         --exists L, w1, w2. split ; [|split ; [|split ; [|split ; [|split]]]] ; 
@@ -2863,8 +2922,8 @@ case (w1 =?= w2) as [Ew12 | NEw12].
       ++assert (Hlr : ((L^min ps + L^max ps) / 2 < L^P w2 \/ L^P w1 < (L^min ps + L^max ps) / 2)%R).
         { rewrite (segment_line L) in Hmiddle.
           + rewrite line_middle in Hmiddle. rewrite line_P_iP in Hmiddle by assumption. lra.
-          + apply Halign, (weber_segment_InA Hweb).
-          + apply Halign, (weber_segment_InA Hweb).
+          + apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
+          + apply Halign, (weber_segment_InA h_psnonnil NEw12 Hweb).
           + apply line_contains_middle ; unfold line_contains ; [now rewrite line_P_iP_min | now rewrite line_P_iP_max]. }
         clear Hmiddle. case Hlr as [Hmiddle | Hmiddle].
         --exists L, w2, w1. split ; [|split ; [|split ; [|split ; [|split]]]] ; 
@@ -2974,8 +3033,27 @@ Ltac fold_all t :=
       H  : _ |- _ => fold t in H
     end); fold t.
 
+Ltac fold_all2 t :=
+  (repeat progress match goal with
+      H  : _ |- _ => progress fold t in H
+    end); fold t.
+
+Lemma line_dir_nonnul_sufficient L ps w1 w2: 
+ps <> nil ->
+  aligned_on L ps ->
+  (forall w : R2, Weber ps w <-> segment w1 w2 w) ->
+  w1 =/= w2 ->
+  line_dir L =/= 0%VS.
+Proof.
+  intros h_nonnil h_align h_web_seg h_neq. 
+  apply (line_dir_nonnul _ w1 w2).
+    - apply h_neq.
+    - apply h_align.
+      apply (@weber_segment_InA _ w1 w2);auto.
+    - apply h_align. apply (@weber_segment_InA _ w1 w2);auto.
+Qed.
+
 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),
@@ -2989,15 +3067,17 @@ Lemma round_simplify_phase3 da c L w1 w2 :
 Proof using lt_0n delta_g0.
 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). 
+fold_all2 ps.
+intros Hinv3 Hsim. assert (Hvalid := inv3_valid Hinv3). 
+assert(line_dir L =/= 0%VS) as HlineDir.
+{ apply (@line_dir_nonnul_sufficient L ps w1 w2);auto; apply Hinv3. }
 destruct (round_simplify Hsim Hvalid) as [r Hround].
-fold_all ps.
+fold_all2 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_2 c).
-fold_all ps.
+fold_all2 ps.
 destruct (weber_calc_seg ps) as [w1' w2'].
 specialize (Hweb' w1' w2' eq_refl).
 assert (Hperm : perm_pairA equiv (w1', w2') (w1, w2)).
@@ -3006,32 +3086,33 @@ case (w1' =?= w2') as [Ew12' | NEw12'].
 + exfalso. apply NEw12. case Hperm as [[H1 H2] | [H1 H2]].
   - rewrite <-H1, <-H2. exact Ew12'.
   - rewrite <-H1, <-H2. symmetry. exact Ew12'.
-+ pose (r1 := L^-P (L^min (pos_list c))). pose (r2 := L^-P (L^max (pos_list c))).
-  destruct (robot_with_mult (Nat.div2 (n+1)) (pos_list c)) as [t|] eqn:E.
++ pose (r1 := L^-P (L^min ps)). pose (r2 := L^-P (L^max ps)).
+  destruct (robot_with_mult (Nat.div2 (n+1)) ps) as [t|] eqn:E.
   - exfalso.
     unfold robot_with_mult in E. apply find_some in E. 
     destruct E as [_ E]. rewrite eqb_true_iff in E.
-    assert (Hps : pos_list c <> nil).
-    { rewrite <-length_zero_iff_nil, pos_list_length. lia. }
-    assert (Ht : InA equiv t (pos_list c)).
-    { rewrite <-multiplicity_pos_InA, multiplicity_countA, E, gt_lt_iff.
+    assert (Hps : ps <> nil).
+    { unfold ps. rewrite <-length_zero_iff_nil, pos_list_length. lia. }
+    assert (Ht : InA equiv t ps).
+    { unfold ps in *. rewrite <-multiplicity_pos_InA, multiplicity_countA, E, gt_lt_iff.
       apply Exp_prop.div2_not_R0. lia. }
-    cut (OnlyWeber (pos_list c) t).
+    cut (OnlyWeber ps t).
     { intros HOW. apply NEw12. transitivity t.
-      * apply HOW. rewrite Hweb. apply segment_start.
+      * apply HOW. fold_all2 ps. rewrite Hweb. apply segment_start.
       * symmetry. apply HOW. rewrite Hweb. apply segment_end. } 
-    assert (aligned_on L (t::(pos_list c))) as halignt.
+    assert (aligned_on L (t::ps)) as halignt.
     { apply aligned_on_cons_iff.
       split.
       - apply aligned_on_InA_contains with ps;auto.
       - assumption. }
-    fold_all ps.
+    fold_all2 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 Halign. unfold ps in *. 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.
+    fold_all2 ps.
+    rewrite line_on_length_aligned;auto.
+    rewrite 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. fold ps. rewrite E. intuition. }
@@ -3050,31 +3131,32 @@ case (w1' =?= w2') as [Ew12' | NEw12'].
         fold ps in Hr1_mult.
         rewrite E in Hr1_mult.
         lia. } 
+    fold_all2 ps.
     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.
-  - pose (L' := line_calc (pos_list c)). fold L'.
-    assert (H_LL' := @line_endpoints_invariant _ _ _ _ _ L L' (pos_list c)).
+    cbn [INR] in Hl1, Hr1. foldR2. unfold Rabs. destruct_match; lra.
+- pose (L' := line_calc ps). fold L'.
+    assert (H_LL' := @line_endpoints_invariant _ _ _ _ _ L L' ps).
     feed_n 3 H_LL'.
-    { rewrite <-length_zero_iff_nil, pos_list_length. lia. }
+    { unfold ps. rewrite <-length_zero_iff_nil, pos_list_length. lia. }
     { exact Halign. }
     { unfold L'. apply line_calc_spec. exists L. exact Halign. }
-    pose (r1' := L'^-P (L'^min (pos_list c))). pose (r2' := L'^-P (L'^max (pos_list c))).
+    pose (r1' := L'^-P (L'^min ps)). pose (r2' := L'^-P (L'^max ps)).
     foldR2. fold r1 r2 r1' r2' in H_LL' |- *.
     assert (Hmiddle_eq : middle r1 r2 == middle r1' r2').
     { case H_LL' as [[-> ->] | [-> ->]] ; [|rewrite middle_comm] ; reflexivity. }
     repeat rewrite <-Hmiddle_eq.
     assert (Hseg : segment w1 w2 (middle r1 r2)).
     { 
-      assert (Hps : pos_list c <> nil).
-      { rewrite <-length_zero_iff_nil, pos_list_length. lia. }
+      assert (Hps : ps <> nil).
+      { unfold ps. rewrite <-length_zero_iff_nil, pos_list_length. lia. }
       rewrite (segment_line L).
       + left. unfold r1, r2. rewrite line_middle. rewrite line_P_iP ; [exact Hmiddle|].
         apply (line_dir_nonnul L w1 w2) ; [assumption | |].
-        - apply weber_aligned with (pos_list c) ; [assumption .. | rewrite Hweb ; apply segment_start].
-        - apply weber_aligned with (pos_list c) ; [assumption .. | rewrite Hweb ; apply segment_end].
-      + apply weber_aligned with (pos_list c) ; [assumption .. | rewrite Hweb ; apply segment_start].
-      + apply weber_aligned with (pos_list c) ; [assumption .. | rewrite Hweb ; apply segment_end].
+        - apply weber_aligned with ps ; [assumption .. | rewrite Hweb ; apply segment_start].
+        - apply weber_aligned with ps ; [assumption .. | rewrite Hweb ; apply segment_end].
+      + apply weber_aligned with ps ; [assumption .. | rewrite Hweb ; apply segment_start].
+      + apply weber_aligned with ps ; [assumption .. | rewrite Hweb ; apply segment_end].
       + apply line_contains_middle. 
         - unfold r1. now apply Halign, line_iP_min_InA.
         - unfold r2. now apply Halign, line_iP_max_InA. 
@@ -3102,8 +3184,9 @@ repeat split ; cbn [fst snd].
 destruct Hinv4 as [Halign [Hweb [Hmiddle [Hstg [Hends [Hr1_mult Hr2_mult]]]]]].
 assert (NEw12 : w1 =/= w2).
 { intros Ew12. rewrite Ew12 in Hmiddle. lra. }
-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'].
+specialize pos_list_non_nil as h_nonnil.
 assert (Hperm : perm_pairA equiv (w1', w2') (w1, w2)).
 { apply segment_eq_iff. intros x. now rewrite <-Hweb', Hweb. }
 case (w1' =?= w2') as [Ew12' | NEw12'].
@@ -3124,10 +3207,18 @@ 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)).
+    { apply aligned_on_cons_iff.
+      split.
+      - eapply aligned_on_InA_contains;eauto.
+      - assumption. }
+    
+    rewrite (@weber_aligned_spec L (pos_list c) t);auto.
+    2:{ specialize weber_segment_InA with (3:=Hweb) as [h1 h2];auto.
+        apply line_dir_nonnul with (x:=w1) (y:=w2);auto. }
+
     assert (Ht_line : line_contains L t).
-    { apply Halign. rewrite <-multiplicity_pos_InA, multiplicity_countA, E.
-      apply Exp_prop.div2_not_R0 ; lia. }
+    { apply Halign;auto. }
     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.
@@ -3547,7 +3638,7 @@ assert (Hinv2' := Hinv2).
 unfold inv2 in Hinv2'. destruct Hinv2' as [Halign [Hw12 [Hr1_mult [Hr2_mult [Hstg Hr2_stay]]]]].
 pose (r1 := L^-P (L^min (pos_list c))). pose (r2 := L^-P (L^max (pos_list c))).
 fold r1 r2 in Hround, Hr1_mult, Hr2_mult, Hr2_stay, Hstg |- *.
-assert (Hweb := weber_calc_seg_correct (pos_list c)).
+assert (Hweb := @weber_calc_seg_correct (pos_list c) (pos_list_non_nil _)).
 assert (Hr1_multR : (!! (round gatherW da c))[r1] >= Nat.div2 (n+1)).
 { rewrite ge_le_iff. transitivity (!! c)[r1].
   + now rewrite Hr1_mult.
@@ -3578,7 +3669,7 @@ apply Nat.le_lteq in Hr1_multR. case Hr1_multR as [Hr1_multR | Hr1_multR].
   apply weber_majority. rewrite pos_list_length, <-multiplicity_countA. rewrite gt_lt_iff.
   eapply Nat.le_lt_trans ; [reflexivity | exact Hr1_multR].
 + unfold inv2. 
-  assert (HwebR := weber_calc_seg_correct (pos_list (round gatherW da c))).
+  assert (HwebR := @weber_calc_seg_correct (pos_list (round gatherW da c)) (pos_list_non_nil _)).
   destruct (weber_calc_seg (pos_list (round gatherW da c))) as [Rw1 Rw2].
   case (Rw1 =?= Rw2) as [ERw | NERw].
   - (* We go to phase 1. This case is actually impossible, but proving it would be rather tedious. *)
@@ -3668,7 +3759,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 ->
+  (* line_dir L <> 0%VS -> *)
   similarity_da_prop da ->
   inv3 c L w1 w2 -> 
   (exists w, inv1 (round gatherW da c) w) \/ 
@@ -3737,8 +3828,8 @@ fold r1 r2 in Hends_max, Hends_min.
 assert (HalignR : aligned_on L (pos_list (round gatherW da c))).
 { apply aligned_preserved with (middle r1 r2) ; try assumption.
   rewrite aligned_on_cons_iff. split ; [now apply line_contains_middle | assumption]. }
-assert (HwebR := weber_calc_seg_correct (pos_list (round gatherW da c))).
-destruct (weber_calc_seg (pos_list (round gatherW da c))) as [Rw1 Rw2].
+assert (HwebR := @weber_calc_seg_correct (pos_list (round gatherW da c)) (pos_list_non_nil _)).
+destruct (@weber_calc_seg (pos_list (round gatherW da c))) as [Rw1 Rw2].
 case (Rw1 =?= Rw2) as [ERw12 | NERw12].
 (* We go to phase 1. *)
 + left. exists (middle r1 r2). split ; [assumption|]. split ; [assumption|].
@@ -3788,7 +3879,7 @@ case (Rw1 =?= Rw2) as [ERw12 | NERw12].
       ++case ifP_bool ; [|intuition]. 
         intros Hcond. exfalso. rewrite orb_true_iff, 2 eqb_true_iff in Hcond.
         rewrite Hid in Hcond. 
-        assert (Hr_Nweb := @inv34_endpoints_not_weber c L w1 w2). cbn zeta in Hr_Nweb.
+        assert (Hr_Nweb := @inv34_endpoints_not_weber c L w1 w2 Hline_dir). cbn zeta in Hr_Nweb.
         feed Hr_Nweb. { auto. } destruct Hr_Nweb as [Hr1_Nweb Hr2_Nweb].
         fold r1 r2 in Hr1_Nweb, Hr2_Nweb.
         case Hcond as [Hcond | Hcond] ; apply Hr1_Nweb ; rewrite <-Hcond, Hweb ; 
@@ -3800,7 +3891,7 @@ case (Rw1 =?= Rw2) as [ERw12 | NERw12].
       ++case ifP_bool ; [|intuition]. 
         intros Hcond. exfalso. rewrite orb_true_iff, 2 eqb_true_iff in Hcond.
         rewrite Hid in Hcond. 
-        assert (Hr_Nweb := @inv34_endpoints_not_weber c L w1 w2). cbn zeta in Hr_Nweb.
+        assert (Hr_Nweb := @inv34_endpoints_not_weber c L w1 w2 Hline_dir). cbn zeta in Hr_Nweb.
         feed Hr_Nweb. { auto. } destruct Hr_Nweb as [Hr1_Nweb Hr2_Nweb].
         fold r1 r2 in Hr1_Nweb, Hr2_Nweb.
         case Hcond as [Hcond | Hcond] ; apply Hr2_Nweb ; rewrite <-Hcond, Hweb ; 
@@ -3889,20 +3980,20 @@ destruct Hends_strong as [Hends_min Hends_max].
 feed Hends_min.
 { destruct (line_bounds L (pos_list c) w1) as [Hbounds _] ; [now apply (@weber_segment_InA _ w1 w2)|].
   case Hbounds ; [intuition|]. rewrite <-Hr1. intros Heq. exfalso. 
-  cut ( Weber (pos_list c) r1). { unfold r1. apply (@inv34_endpoints_not_weber c L w1 w2). now right. }
+  cut ( Weber (pos_list c) r1). { unfold r1. apply (@inv34_endpoints_not_weber c L w1 w2 Hline_dir). now right. }
   apply (f_equal (L^-P)) in Heq. rewrite Hr1 in Heq. fold r1 in Heq. rewrite Hline_w1 in Heq.
   rewrite Heq, Hweb. apply segment_start. }
 feed Hends_max.
 { destruct (line_bounds L (pos_list c) w1) as [_ Hbounds] ; [now apply (@weber_segment_InA _ w1 w2)|].
   case Hbounds ; [intuition|]. rewrite <-Hr2. intros Heq. exfalso. 
-  cut ( Weber (pos_list c) r2). { unfold r2. apply (@inv34_endpoints_not_weber c L w1 w2). now right. }
+  cut ( Weber (pos_list c) r2). { unfold r2. apply (@inv34_endpoints_not_weber c L w1 w2 Hline_dir). now right. }
   apply (f_equal (L^-P)) in Heq. rewrite Hr2 in Heq. fold r2 in Heq. rewrite Hline_w1 in Heq.
   rewrite <-Heq, Hweb. apply segment_start. }
 fold r1 r2 in Hends_max, Hends_min.
 assert (HalignR : aligned_on L (pos_list (round gatherW da c))).
 { apply aligned_preserved with w1 ; try assumption.
   rewrite aligned_on_cons_iff. intuition. }
-assert (HwebR := weber_calc_seg_correct (pos_list (round gatherW da c))).
+assert (HwebR := @weber_calc_seg_correct (pos_list (round gatherW da c)) (pos_list_non_nil _)).
 destruct (weber_calc_seg (pos_list (round gatherW da c))) as [Rw1 Rw2].
 case (Rw1 =?= Rw2) as [ERw12 | NERw12].
 (* We go to phase 1. *)
@@ -3953,7 +4044,7 @@ case (Rw1 =?= Rw2) as [ERw12 | NERw12].
   - rewrite <-segment_eq_iff in HRw_perm. rewrite <-Hw1_stay. setoid_rewrite HRw_perm. exact HwebR.
   - rewrite <-Hw1_stay, Hr1_stay, Hr2_stay. split ; [|assumption]. rewrite Hw1_stay. apply Hmiddle.
   - assumption.
-  - assert (Hr_Nweb := @inv34_endpoints_not_weber c L w1 w2). cbn zeta in Hr_Nweb.
+  - assert (Hr_Nweb := @inv34_endpoints_not_weber c L w1 w2 Hline_dir). cbn zeta in Hr_Nweb.
     feed Hr_Nweb. { auto. } destruct Hr_Nweb as [Hr1_Nweb Hr2_Nweb].
     fold r1 r2 in Hr1_Nweb, Hr2_Nweb.
     split. 
@@ -4294,8 +4385,8 @@ feed_n 4 Hends.
   + generalize (line_min_le_max L (pos_list c)). lra.
   + apply line_dir_nonnul with w1 w2.
     - apply Hinv3.
-    - apply Hinv3, (@weber_segment_InA _ w1 w2). apply Hinv3.
-    - apply Hinv3, (@weber_segment_InA _ w1 w2). apply Hinv3. }
+    - apply Hinv3, (@weber_segment_InA _ w1 w2);auto;apply Hinv3.
+    - apply Hinv3, (@weber_segment_InA _ w1 w2);auto;apply Hinv3. }
 destruct Hends as [Hends_min Hends_max].
 unfold measure. case (get_location (c id) =?= (middle r1 r2)) as [Hloc | Hloc].
 + apply Rplus_le_compat_eps_2. 
@@ -4315,6 +4406,23 @@ unfold measure. case (get_location (c id) =?= (middle r1 r2)) as [Hloc | Hloc].
     * unfold r1, r2. rewrite <-Hends_min, <-Hends_max. apply Hinv3R.
 Qed.
 
+Lemma inv4_diff c L w1 w2: inv4 c L w1 w2 ->  w1 =/= w2.
+Proof.
+  intros Hinv4.
+  intros Ew12. rewrite Ew12 in Hinv4.
+  unfold inv4 in Hinv4.
+  decompose [and] Hinv4; clear Hinv4.
+  lra.
+Qed. 
+
+Lemma inv3_diff c L w1 w2: inv3 c L w1 w2 ->  w1 =/= w2.
+Proof.
+  intros Hinv3.
+  red in Hinv3.
+  decompose [and] Hinv3; clear Hinv3.
+  assumption.
+Qed. 
+
 Lemma phase4_decrease c da L w1 w2 : 
   let r1 := L^-P (L^min (pos_list c)) in 
   let r2 := L^-P (L^max (pos_list c)) in 
@@ -4332,13 +4440,16 @@ intros Hsim Hflex Hinv4 [w1' [w2' Hinv4R]] [id [Hact HNloop]].
 assert (Hvalid := inv4_valid Hinv4).
 assert (Hnil : pos_list c <> nil).
 { rewrite <-length_zero_iff_nil, pos_list_length. lia. }
+assert (Hdiff : w1 =/= w2) by apply (inv4_diff Hinv4).
+
 assert (Hends := @endpoints_preserved da L c w1 Hsim Hvalid).
 feed_n 4 Hends.
 { rewrite aligned_on_cons_iff. split ; [apply Hinv4 | now apply Hinv4].
-  apply (@weber_segment_InA _ w1 w2). apply Hinv4. }
+  apply (@weber_segment_InA _ w1 w2);auto;try apply Hinv4. }
 { apply Hinv4. }
 { apply Hinv4. }
-{ apply line_bounds. apply (@weber_segment_InA _ w1 w2). apply Hinv4. }
+
+{ apply line_bounds. apply (@weber_segment_InA _ w1 w2);auto. apply Hinv4. }
 destruct Hends as [Hends_min Hends_max].
 unfold measure. foldR2. case (get_location (c id) =?= w1) as [Hloc | Hloc].
 + apply Rplus_le_compat_eps_2. 
@@ -4507,9 +4618,11 @@ assert (Hw12 : exists id,
   get_location (c id) =/= middle r1 r2).
 { 
   assert (Hw1 : exists id, w1 == get_location (c id)).
-  { rewrite <-pos_list_InA. apply (@weber_segment_InA _ w1 w2), Hinv3. }
+  { rewrite <-pos_list_InA. apply (@weber_segment_InA _ w1 w2);try apply Hinv3.
+    apply pos_list_non_nil. }
   assert (Hw2 : exists id, w2 == get_location (c id)).
-  { rewrite <-pos_list_InA. apply (@weber_segment_InA _ w1 w2), Hinv3. }  
+  { rewrite <-pos_list_InA. apply (@weber_segment_InA _ w1 w2);try apply  Hinv3.
+    apply pos_list_non_nil. }  
   assert (Hmiddle : w1 =/= middle r1 r2 \/ w2 =/= middle r1 r2).  
   { case (w1 =?= middle r1 r2) as [H1 | H1] ; 
     case (w2 =?= middle r1 r2) as [H2 | H2] ; intuition ; [].
@@ -4563,7 +4676,9 @@ intros Hfair Hsim Hinv4. destruct (Hfair) as [Hfair_now _].
 remember (L^-P (L^min (pos_list c))) as r1.
 remember (L^-P (L^max (pos_list c))) as r2.
 assert (Hid : exists id, w2 == get_location (c id)).
-{ rewrite <-pos_list_InA. apply (@weber_segment_InA _ w1 w2), Hinv4. }
+{ rewrite <-pos_list_InA. apply (@weber_segment_InA _ w1 w2);try apply Hinv4.
+  - apply pos_list_non_nil.
+  - apply (inv4_diff Hinv4). }
 destruct Hid as [id Hid].
 revert c w2 Hinv4 Heqr1 Heqr2 Hid.
 induction (Hfair_now id) as [d Hact | d Hlater IH] ; intros c w2 Hinv4 Heqr1 Heqr2 Hid.
@@ -4874,10 +4989,8 @@ clear Hsim_hd. feed_n 4 Hends.
 { rewrite Heqr1, Heqr2. apply Hinv3. }
 { rewrite Heqr1, Heqr2. rewrite line_middle. rewrite line_P_iP.
   + generalize (line_min_le_max L (pos_list c)). lra.
-  + apply (line_dir_nonnul _ w1 w2).
-    - apply Hinv3.
-    - apply Hinv3, (@weber_segment_InA _ w1 w2), Hinv3.
-    - apply Hinv3, (@weber_segment_InA _ w1 w2), Hinv3. }
+  + apply (@line_dir_nonnul_sufficient L (pos_list c) w1 w2);try apply Hinv3.
+    apply pos_list_non_nil. }
 destruct Hends as [Hends_min Hends_max].
 assert (Hprogress := phase3_progress Hfair Hsim Hinv3).
 apply first_move_strengthen in Hprogress ; [|assumption | assumption | right ; right ; left ; eauto].
@@ -4916,10 +5029,8 @@ induction Hprogress as [d c id Hact HNloop | d c Hlater IH2].
   { rewrite Heqr1, Heqr2, <-Hends_min, <-Hends_max. apply Hinv3R. }
   { rewrite Heqr1, Heqr2, Hends_min, Hends_max. rewrite line_middle. rewrite line_P_iP.
     + generalize (line_min_le_max L (pos_list c)). lra.
-    + apply (line_dir_nonnul _ w1 w2).
-      - apply Hinv3.
-      - apply Hinv3, (@weber_segment_InA _ w1 w2), Hinv3.
-      - apply Hinv3, (@weber_segment_InA _ w1 w2), Hinv3. }
+    +  apply (@line_dir_nonnul_sufficient L (pos_list c) w1 w2);try apply Hinv3.
+       apply  pos_list_non_nil. }
   destruct HendsR as [HendsR_min HendsR_max].
   apply Stream.Later, IH2 ; try assumption.
   - now rewrite Hends_min, Heqr1. 
@@ -4972,10 +5083,14 @@ assert (Hnil : pos_list c <> nil).
 assert (Hends := @endpoints_preserved (Stream.hd d) L c w1 Hsim_hd (inv4_valid Hinv4)).
 clear Hsim_hd. feed_n 4 Hends.
 { rewrite aligned_on_cons_iff. split ; [|now apply Hinv4]. 
-  apply Hinv4, (@weber_segment_InA _ w1 w2), Hinv4. }
+  apply Hinv4, (@weber_segment_InA _ w1 w2); try apply Hinv4.
+  - apply pos_list_non_nil.
+  - apply (inv4_diff Hinv4). }
 { apply Hinv4. }
 { apply Hinv4. }
-{ apply line_bounds. apply (@weber_segment_InA _ w1 w2), Hinv4. }
+{ apply line_bounds. apply (@weber_segment_InA _ w1 w2);try apply Hinv4.
+  - apply pos_list_non_nil.
+  - apply (inv4_diff Hinv4). }
 destruct Hends as [Hends_min Hends_max].
 assert (Hprogress := phase4_progress Hfair Hsim Hinv4).
 apply first_move_strengthen in Hprogress ; [|assumption | assumption | right ; right ; right ; eauto].
@@ -5005,10 +5120,14 @@ induction Hprogress as [d c id Hact HNloop | d c Hlater IH2].
   feed_n 5 HendsR.
   { eapply inv4_valid. eauto. }
   { rewrite aligned_on_cons_iff. split ; [apply Hinv4R | now apply Hinv4R].
-    apply (@weber_segment_InA _ w1 w2'), Hinv4R. } 
+    apply (@weber_segment_InA _ w1 w2'); try apply Hinv4R.
+    - apply pos_list_non_nil.
+    - apply (inv4_diff Hinv4R). } 
   { apply Hinv4R. }
   { apply Hinv4R. }
-  { apply line_bounds, (@weber_segment_InA _ w1 w2'), Hinv4R. }
+  { apply line_bounds, (@weber_segment_InA _ w1 w2'); try apply Hinv4R.
+    - apply pos_list_non_nil.
+    - apply (inv4_diff Hinv4R). }
   destruct HendsR as [HendsR_min HendsR_max].
   apply Stream.Later, IH2 ; try assumption.
   - intros c' Hc'. apply IH. unfold lt_config in Hc' |- *.
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index db7d8e5b79f134d938ed73502209cb218ff98977..dc74f81ebdeb93bf8b08253fd55c3bdd4a6c2e6e 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -3109,7 +3109,7 @@ Proof.
 
   assert (Nat.Even (length ps)).
   { eapply left_right_balanced_even with (w := pt) (L:=L);try lra. }
-  apply Nat.Even_Odd_False with (Rlength ps);auto.
+  apply Nat.Even_Odd_False with (length ps);auto.
 Qed.