diff --git a/CaseStudies/Gathering/InR2/Algorithm_withLight.v b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
index 8ca2917f68be4a513f68c35c7ed1182be26ec487..67f620dade07cd575bfb93f71b71cf1906694ae8 100644
--- a/CaseStudies/Gathering/InR2/Algorithm_withLight.v
+++ b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
@@ -2160,6 +2160,430 @@ Section SSYNC_Results.
 Variable da : similarity_da.
 Hypothesis Hssync : SSYNC_da da.
 
+(* Robots partitionned wrt to their location, activation and color. *)
+Definition light_on l pt config :=
+  List.filter (fun id => get_light (config id) ==b l) (on_loc pt config).
+Notation black_on := (light_on false).
+Notation white_on := (light_on true).
+Definition active_on pt config :=
+  List.filter (fun id => equiv_decb (get_location (config id)) pt) (active da).
+Definition idle_on pt config :=
+  List.filter (fun id => equiv_decb (get_location (config id)) pt) (idle da).
+Definition light_active_on l pt config :=
+  List.filter (fun id => get_light (config id) ==b l) (active_on pt config).
+Notation black_active_on := (light_active_on false).
+Notation white_active_on := (light_active_on true).
+Definition light_idle_on l pt config :=
+  List.filter (fun id => get_light (config id) ==b l) (idle_on pt config).
+Notation black_idle_on := (light_idle_on false).
+Notation white_idle_on := (light_idle_on true).
+
+Lemma active_on_split : forall pt config,
+  PermutationA equiv (active_on pt config) (black_active_on pt config ++ white_active_on pt config).
+Proof using .
+intros pt config. unfold black_active_on, white_active_on.
+induction (active_on pt) as [| id l]; cbn [List.filter]; try reflexivity; [].
+do 2 destruct_match; cbn [app].
+- reflect_bool. congruence.
+- now constructor.
+- rewrite <- PermutationA_middle; autoclass.
+  now constructor.
+- exfalso. destruct (get_light (config id)); cbn in *; discriminate.
+Qed.
+
+Lemma idle_on_split : forall pt config,
+  PermutationA equiv (idle_on pt config) (black_idle_on pt config ++ white_idle_on pt config).
+Proof using .
+intros pt config. unfold black_idle_on, white_idle_on.
+induction (idle_on pt) as [| id l]; cbn [List.filter]; try reflexivity; [].
+do 2 destruct_match; cbn [app].
+- reflect_bool. congruence.
+- now constructor.
+- rewrite <- PermutationA_middle; autoclass.
+  now constructor.
+- exfalso. destruct (get_light (config id)); cbn in *; discriminate.
+Qed.
+
+Lemma on_loc_split : forall pt config,
+  PermutationA equiv (on_loc pt config) (active_on pt config ++ idle_on pt config).
+Proof using .
+intros pt config. symmetry.
+unfold on_loc, active_on, active, idle_on, idle.
+induction names as [| id l]; cbn [List.filter]; try reflexivity; [].
+do 2 (destruct_match; cbn [app List.filter negb]).
+- now constructor.
+- apply IHl.
+- rewrite <- PermutationA_middle; autoclass.
+  now constructor.
+- apply IHl.
+Qed.
+
+Instance on_loc_compat : Proper (equiv ==> equiv ==> eq) on_loc.
+Proof using .
+intros pt1 pt2 Hpt config1 config2 Hconfig.
+unfold on_loc.
+apply ListComplements.filter_extensionality_compat.
+- intros xx id ?. subst xx. now rewrite Hconfig, Hpt.
+- reflexivity.
+Qed.
+
+Instance Light_on_compat : Proper (eq ==> equiv ==> equiv ==> eq) light_on.
+Proof using .
+intros xx l ? pt1 pt2 Hpt config1 config2 Hconfig. subst xx.
+unfold light_on.
+apply ListComplements.filter_extensionality_compat.
+- intros xx id ?. subst xx. now rewrite Hconfig.
+- now f_equiv.
+Qed.
+
+Lemma length_light_on : forall l pt config,
+  length (light_on l pt config) = (colors (snd (!!! (config, (0%VS, witness)))))[(pt, l)].
+Proof using .
+intros l pt config. destruct (obs_from_config_spec config (0%VS, witness)) as [_ [_ Hobs]].
+rewrite Hobs, config_list_spec, count_filter_length, filter_map, map_length.
+unfold black_on, on_loc. rewrite <- filter_andb. f_equal. f_equiv.
+intros xx id ?. subst xx. clear.
+symmetry. destruct_match; symmetry.
+- revert_one @equiv. intros [Heq1 Heq2]. unfold get_light. simpl get_location.
+  rewrite Heq1, Heq2. now simpl_bool.
+- reflect_bool. destruct (get_light (config id) =?= l); firstorder.
+Qed.
+
+Lemma on_loc_color_split : forall pt config,
+  PermutationA equiv (on_loc pt config) (black_on pt config ++ white_on pt config).
+Proof using .
+intros pt config.
+unfold light_on, on_loc.
+induction names as [| id l]; cbn [List.filter]; try reflexivity; [].
+repeat (destruct_match; cbn [app List.filter]); reflect_bool.
+- congruence.
+- now constructor.
+- rewrite <- PermutationA_middle; autoclass.
+  now constructor.
+- destruct (get_light (config id)); intuition.
+- assumption.
+Qed.
+
+(* TODO: use have_obs everywhere
+   TODO: make a tactic to reorder filtering *)
+
+Lemma active_on_loc_swap : forall pt config,
+  List.filter (activate da) (on_loc pt config) = active_on pt config.
+Proof using .
+intros pt config.
+unfold on_loc, active_on, active.
+rewrite <- 2 filter_andb.
+apply ListComplements.filter_extensionality_compat.
+- repeat intro. subst. apply andb_comm.
+- reflexivity.
+Qed.
+
+Lemma idle_on_loc_swap : forall pt config,
+  List.filter (fun id => negb (activate da id)) (on_loc pt config) = idle_on pt config.
+Proof using .
+intros pt config.
+unfold on_loc, idle_on, idle.
+rewrite <- 2 filter_andb.
+apply ListComplements.filter_extensionality_compat.
+- repeat intro. subst. apply andb_comm.
+- reflexivity.
+Qed.
+
+Lemma on_loc_color_swap : forall config pt l id_l,
+  List.filter (fun id => get_location (config id) ==b pt)
+    (List.filter (fun id => get_light (config id) ==b l) id_l)
+  = List.filter (fun id => get_light (config id) ==b l)
+      (List.filter (fun id => get_location (config id) ==b pt) id_l).
+Proof using .
+intros config pt l id_l.
+rewrite <- 2 filter_andb.
+apply ListComplements.filter_extensionality_compat.
+- repeat intro. subst. apply andb_comm.
+- reflexivity.
+Qed.
+
+Lemma on_loc_split_active_colors : forall pt config,
+  PermutationA equiv (on_loc pt config)
+    (active_on pt config ++ black_idle_on pt config ++ white_idle_on pt config).
+Proof using .
+intros pt config.
+assert (Hperm := partition_PermutationA (eqA := equiv) (activate da) (on_loc pt config)).
+rewrite <- Hperm, partition_filter, active_on_loc_swap, idle_on_loc_swap.
+cbn [fst snd]. f_equiv.
+unfold idle_on.
+assert (Hperm' := partition_PermutationA (eqA := equiv) (fun id =>  get_light (config id) ==b false) (idle da)).
+rewrite <- Hperm', partition_filter.
+cbn [fst snd].
+rewrite filter_app. f_equiv.
++ now rewrite on_loc_color_swap.
++ assert (Heq : (eq ==> eq)%signature (fun id => negb (get_light (config id) ==b false))
+                                      (fun id => get_light (config id) ==b true)).
+  { intros xx id ?. subst xx. now destruct (get_light (config id)). }
+  rewrite Heq, on_loc_color_swap.
+  reflexivity.
+Qed.
+
+Hint Resolve pos_in_config mult_div2_In color_bivalent_bivalent : core.
+
+
+Section BivalentResults.
+
+Variable config : configuration.
+Hypothesis Hbivalent : bivalent config.
+
+Definition loc_g1 := get_location (config (Good g1)).
+Definition loc_others := find_other_loc (!!config) loc_g1.
+
+Notation active_on_g1 := (active_on loc_g1 config).
+Notation active_on_other := (active_on loc_others config).
+Notation idle_on_g1 := (idle_on loc_g1 config).
+Notation idle_on_other := (idle_on loc_others config).
+Notation black_active_on_g1 := (black_active_on loc_g1 config).
+Notation black_active_on_other := (black_active_on loc_others config).
+Notation white_active_on_g1 := (white_active_on loc_g1 config).
+Notation white_active_on_other := (white_active_on loc_others config).
+Notation black_idle_on_g1 := (black_idle_on loc_g1 config).
+Notation black_idle_on_other := (black_idle_on loc_others config).
+Notation white_idle_on_g1 := (white_idle_on loc_g1 config).
+Notation white_idle_on_other := (white_idle_on loc_others config).
+Notation black_on_g1 := (black_on loc_g1 config).
+Notation black_on_other := (black_on loc_others config).
+Notation white_on_g1 := (white_on loc_g1 config).
+Notation white_on_other := (white_on loc_others config).
+
+(* Some trivial lemmas that are overused *)
+ 
+Lemma bivalent_even : Nat.Even (nG + nB).
+Proof using Hbivalent. now destruct Hbivalent. Qed.
+
+Local Definition loc_g1_In : In loc_g1 (!! config) := pos_in_config _ _ _.
+Local Definition loc_g1_In_fst : forall st, In loc_g1 (fst (!!! (config, st))) := fun st => pos_in_config _ st _.
+
+Local Lemma loc_others_In : In loc_others (!! config).
+Proof using Hbivalent.
+rewrite <- support_spec, obs_fst, find_other_loc_spec.
+- now right; left.
+- now rewrite bivalent_obs_spec.
+- apply pos_in_config.
+Qed.
+
+Local Lemma loc_others_In_fst : forall st, In loc_others (fst (!!! (config, st))).
+Proof using Hbivalent. intro. apply loc_others_In. Qed.
+
+Local Lemma In_fst_config : forall id, In (get_location (config id)) (fst (!!! (config, (0%VS, witness)))).
+Proof using . intro id. apply pos_in_config. Qed.
+
+Local Lemma loc_g1_diff_others: loc_g1 =/= loc_others.
+Proof using Hbivalent.
+unfold loc_others.
+symmetry.
+rewrite obs_fst.
+apply find_other_loc_diff.
+- now apply bivalent_obs_spec.
+- apply pos_in_config.
+Qed.
+
+Local Lemma loc_others_diff_g1 : loc_others =/= loc_g1.
+Proof using Hbivalent.
+unfold loc_others. rewrite obs_fst. apply find_other_loc_diff.
+- now rewrite bivalent_obs_spec.
+- apply loc_g1_In_fst.
+Qed.
+
+Local Lemma other_than_loc_g1 : forall id, get_location (config id) =/= loc_g1 -> get_location (config id) == loc_others.
+Proof using Hbivalent.
+intros.
+eapply (bivalent_same_location (0%VS, witness) Hbivalent (pt3 := loc_g1)).
+- apply pos_in_config.
+- apply loc_others_In_fst.
+- apply pos_in_config.
+- assumption.
+- symmetry. apply loc_g1_diff_others.
+Qed.
+
+Local Lemma other_than_loc_others : forall id, get_location (config id) =/= loc_others -> get_location (config id) == loc_g1.
+Proof using Hbivalent.
+intros.
+eapply (bivalent_same_location (0%VS, witness) Hbivalent (pt3 := loc_others)).
+- apply pos_in_config.
+- apply pos_in_config.
+- apply loc_others_In_fst.
+- assumption.
+- apply loc_g1_diff_others.
+Qed.
+
+Corollary find_other_loc_loc_others : find_other_loc (!! config) loc_others == loc_g1.
+Proof using Hbivalent.
+assert (Hin : In (find_other_loc (fst (!!! (config, (0%VS, witness)))) loc_others) (!! config)).
+{ apply find_other_loc_In.
+  - now rewrite bivalent_obs_spec.
+  - apply loc_others_In. }
+rewrite obs_from_config_In in Hin. destruct Hin as [id Hid].
+rewrite <- Hid. apply other_than_loc_others.
+rewrite Hid. apply find_other_loc_diff.
+- now rewrite bivalent_obs_spec.
+- apply loc_others_In.
+Qed.
+
+Local Lemma have_support : PermutationA equiv (support (!! (config))) (cons loc_g1 (cons loc_others nil)).
+Proof using Hbivalent.
+rewrite obs_fst.
+apply find_other_loc_spec.
+- now rewrite bivalent_obs_spec.
+- apply loc_g1_In_fst.
+Qed.
+
+Local Lemma loc_g1_mult : (!! config)[loc_g1] = Nat.div2 (nG + nB).
+Proof using Hbivalent.
+apply extend_bivalent in Hbivalent.
+destruct Hbivalent as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 [_ [Hin _]]]]]]]]].
+changeR2. specialize (Hin _ loc_g1_In).
+now destruct Hin as [Heq | Heq]; rewrite Heq.
+Qed.
+
+Local Lemma loc_others_mult : (!! config)[loc_others] = Nat.div2 (nG + nB).
+Proof using Hbivalent.
+assert (Hbiv := proj1 (extend_bivalent _) Hbivalent).
+destruct Hbiv as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 [_ [Hin _]]]]]]]]].
+changeR2. specialize (Hin _ loc_others_In).
+now destruct Hin as [Heq | Heq]; rewrite Heq.
+Qed.
+
+Lemma bivalent_In_iff_mult_eq_half :
+  forall pt, In pt (!! config) <-> (!! config)[pt] = Nat.div2 (nG + nB).
+Proof using size_G Hbivalent.
+intro pt. split; intro Hin.
++ rewrite <- support_spec in Hin.
+  apply extend_bivalent in Hbivalent.
+  destruct Hbivalent as [_ [_ [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 [Hsupp [Hin_supp Hother]]]]]]]]].
+  changeR2. rewrite Hsupp, InA_cons, InA_singleton in Hin.
+  destruct Hin as [Heq | Heq]; rewrite Heq; auto.
++ unfold In. rewrite Hin. auto.
+Qed.
+
+Lemma loc_g1_or_loc_others_eqb : forall id,
+  get_location (config id) ==b loc_others = negb (get_location (config id) ==b loc_g1).
+Proof using Hbivalent.
+intro id. unfold loc_others.
+destruct (get_location (config id) ==b loc_g1) eqn:Hcase; cbn [negb]; reflect_bool.
++ rewrite Hcase, obs_fst.
+  symmetry. apply find_other_loc_diff.
+  - now rewrite bivalent_obs_spec.
+  - apply pos_in_config.
++ apply (bivalent_same_location (0%VS, witness) Hbivalent (pt3 := loc_g1)).
+  - apply pos_in_config.
+  - rewrite obs_fst.
+    apply find_other_loc_In, pos_in_config.
+    now rewrite bivalent_obs_spec.
+  - apply loc_g1_In.
+  - assumption.
+  - rewrite obs_fst.
+    apply find_other_loc_diff, pos_in_config.
+    now rewrite bivalent_obs_spec.
+Qed.
+
+Corollary bivalent_get_location_cases : forall id,
+  get_location (config id) == loc_g1 \/ get_location (config id) == loc_others.
+Proof using Hbivalent.
+intro id.
+assert (Hbool := loc_g1_or_loc_others_eqb id).
+destruct (get_location (config id) ==b loc_g1) eqn:Hcase.
+- left. now reflect_bool.
+- right. now reflect_bool.
+Qed.
+
+(* TODO: see if it is useful elsewhere *)
+Lemma wlog_sym : forall (x y : location) P, Proper (equiv ==> equiv ==> iff) P ->
+  (P x y -> P y x) ->
+  forall x' y', PermutationA equiv (cons x (cons y nil)) (cons x' (cons y' nil)) ->
+  P x y -> P x' y'.
+Proof using .
+intros x y P HP Hsym x' y' Hperm HPxy.
+rewrite PermutationA_2 in Hperm; auto; [].
+ destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite <- Heq1, <- Heq2; auto.
+Qed.
+
+Lemma find_max_black_comm : ~ color_bivalent config ->
+  forall st pt1 pt2,
+    In pt1 (!! config) -> In pt2 (!! config) ->
+    find_max_black (!!! (config, st)) pt1 pt2 == find_max_black (!!! (config, st)) pt2 pt1.
+Proof using size_G Hbivalent.
+intros Hcolor st pt1 pt2 Hin1 Hin2. unfold find_max_black.
+repeat destruct_match; try reflexivity || (rewrite Nat.leb_gt in *; lia); [].
+destruct (pt1 =?= pt2) as [? | Hneq]; auto; [].
+exfalso. apply Hcolor.
+assert (Hbiv := Hbivalent). destruct Hbiv as [Heven [Hn [pt1' [pt2' [Hdiff [Hpt1' Hpt2']]]]]].
+repeat split; trivial; [].
+exists pt1', pt2'. repeat split; trivial; [].
+assert (Heq : (colors (snd (!!! (config, st))))[(pt1, false)]
+            = (colors (snd (!!! (config, st))))[(pt2, false)]).
+{ rewrite Nat.leb_le in *. lia. }
+pattern pt1', pt2'.
+apply (@wlog_sym pt1 pt2).
++ intros ? ? Heq1 ? ? Heq2. rewrite 2 Forall_forall. now rewrite Heq1, Heq2.
++ rewrite 2 Forall_forall. intros Hsym l Hl. symmetry; auto.
++ transitivity (support (!! config)); rewrite obs_fst; changeR2.
+  - symmetry. apply bivalent_support; auto.
+  - apply bivalent_support; auto; rewrite <- obs_fst; now apply mult_div2_In.
++ rewrite Forall_forall. intros [] _; trivial; [].
+  (* white *)
+  rewrite <- 2 length_light_on in *.
+  rewrite 2 (colors_indep config (0%VS, witness) (0%VS, witness)), <- 2 length_light_on in Heq.
+  rewrite bivalent_In_iff_mult_eq_half in Hin1, Hin2; auto.
+  assert (Hlen : length (on_loc pt1 config) = length (on_loc pt2 config)).
+  { now rewrite <- (obs_from_config_on_loc _ (0%VS, witness)), Hin1, <- Hin2, obs_from_config_on_loc. }
+  rewrite (on_loc_color_split pt1 config), (on_loc_color_split pt2 config), 2 app_length in Hlen.
+  lia.
+Qed.
+
+Hint Resolve bivalent_even pos_in_config loc_g1_In loc_g1_In_fst loc_others_In loc_others_In_fst
+             In_fst_config loc_others_diff_g1 loc_g1_mult loc_others_mult loc_g1_diff_others
+             other_than_loc_g1 other_than_loc_others mult_div2_In color_bivalent_bivalent : core.
+
+Definition active_partition :=
+  List.partition (fun id => equiv_decb (get_location (config id)) loc_g1) (active da).
+
+Lemma active_partition_spec : active_partition = (active_on_g1, active_on_other).
+Proof using Hbivalent.
+unfold active_on, active_partition.
+rewrite partition_filter. f_equal.
+rewrite <- eqlistA_Leibniz.
+apply filter_extensionalityA_compat; try reflexivity; [].
+intros xx id ?. subst xx. unfold loc_others. symmetry.
+destruct (get_location (config id) ==b loc_g1) eqn:Hcase; reflect_bool.
++ rewrite Hcase. symmetry. rewrite obs_fst.
+  apply find_other_loc_diff; auto.
+  rewrite bivalent_obs_spec; auto.
++ eapply (bivalent_same_location (0%VS, witness) Hbivalent (pt3 := loc_g1)); auto.
+Qed.
+
+Lemma active_split : PermutationA equiv (active_on_g1 ++ active_on_other) (active da).
+Proof using Hbivalent.
+  replace active_on_g1 with (fst active_partition).
+  replace active_on_other with (snd active_partition).
+  { apply partition_PermutationA. }
+  { now rewrite active_partition_spec. }
+  { now rewrite active_partition_spec. }
+Qed.
+
+Lemma idle_split: PermutationA equiv (idle da) (idle_on_g1 ++ idle_on_other).
+Proof using Hbivalent.
+unfold idle_on.
+induction (idle da); cbn [List.filter]; try reflexivity; [].
+rewrite loc_g1_or_loc_others_eqb; auto; [].
+changeR2. destruct_match; cbn [negb app].
+- now constructor.
+- rewrite <- PermutationA_middle; autoclass.
+  now constructor.
+Qed.
+
+End BivalentResults.
+
+Hint Resolve bivalent_even pos_in_config loc_g1_In loc_g1_In_fst loc_others_In loc_others_In_fst
+             In_fst_config loc_others_diff_g1 loc_g1_mult loc_others_mult loc_g1_diff_others
+             other_than_loc_g1 other_than_loc_others mult_div2_In color_bivalent_bivalent : core.
+
+
 (** We express the behavior of the algorithm in the global (demon) frame of reference. *)
 Theorem round_simplify : forall config,
   round gatherR2 da config
@@ -2168,12 +2592,11 @@ Theorem round_simplify : forall config,
      then
        let obs := !!!(config, config id) in
        if bivalent_obs obs
-       then let other_loc := find_other_loc (fst obs) (get_location (config id)) in
-            if color_bivalent_obs obs
+       then if color_bivalent_obs obs
             then if observer_lght (snd obs)
-                 then (middle (get_location (config id)) other_loc, false)
+                 then (middle (loc_g1 config) (loc_others config), false)
                  else (get_location (config id), true) (* was: (other_loc, true) *)
-            else let maj_black := find_max_black obs (get_location (config id)) other_loc in
+            else let maj_black := find_max_black obs (loc_g1 config) (loc_others config) in
                  (maj_black, observer_lght (snd obs))
        else match support (max (fst obs)) with
               | nil => config id (* only happen with no robots *)
@@ -2221,47 +2644,75 @@ assert (Hcol_biv : color_bivalent_obs local_obs = color_bivalent_obs global_obs)
 assert (Hlight : observer_lght (snd local_obs) = observer_lght (snd global_obs)) by now rewrite Hobs.
 rewrite Hbiv, Hcol_biv, Hlight.
 change new_frame with (sim_f sim).
-destruct (bivalent_obs global_obs) eqn:Hcase_biv;
-[destruct (color_bivalent_obs global_obs) eqn:Hcase_col_biv;
-[destruct (observer_lght (snd global_obs)) eqn:Hcase_light |] |].
-* (* color bivalent and white observer *)
-  split; try reflexivity; [].
-  cbn -[equiv middle inverse].
-  transitivity (middle (sim ⁻¹ 0%VS) (sim ⁻¹ (find_other_loc (fst local_obs) 0%VS))).
-  + now rewrite R2_middle_morph.
-  + apply middle_compat.
-    - change ((sim ⁻¹) 0%VS) with (center (change_frame da config g)). now rewrite similarity_center.
-    - rewrite Hcenter, Hobs. cbn [fst]. rewrite find_other_loc_morph.
-      apply Bijection.retraction_section.
-* (* color bivalent and black observer *)
-  rewrite Hcenter. split; try reflexivity; [].
-  apply Bijection.retraction_section.
-* (* bivalent but not color bivalent *)
-  split; try reflexivity; []. cbn -[equiv inverse].
-  transitivity (find_max_black (map (sim ⁻¹) (fst local_obs), map_light (sim ⁻¹) (snd local_obs))
-                               ((sim ⁻¹) 0%VS) ((sim ⁻¹) (find_other_loc (fst local_obs) 0%VS))).
-  { symmetry. apply find_max_black_morph. }
-  f_equiv.
-  + split; cbn -[equiv].
-    - rewrite Hobs. cbn -[equiv]. rewrite map_merge; autoclass; [].
-      setoid_rewrite <- map_id at 3.
-      apply map_extensionality_compat; try (now repeat intro); [].
-      apply Bijection.retraction_section.
-    - (* FIXME: rewrite Hobs fails here *)
-      transitivity (map_light (Bijection.retraction sim)
-                      (snd (map new_frame (fst global_obs), map_light new_frame (snd global_obs)))).
-      { now apply map_light_compat, snd_compat_pactole. }
-      cbn [snd]. rewrite map_light_merge; trivial.
-      transitivity (map_light id (snd global_obs)); [| now apply map_light_id].
-      apply map_light_extensionality_compat; try (now repeat intro); [].
-      apply Bijection.retraction_section.
-  + apply (similarity_center da).
-  + (* TODO: perform the rewrite in the other direction *)
-    rewrite <- find_other_loc_morph. f_equiv.
-    - rewrite Hobs. cbn [fst]. rewrite map_merge; auto; [].
-      setoid_rewrite <- map_id at 3. apply map_extensionality_compat; [now autoclass |].
-      apply Bijection.retraction_section.
+destruct (bivalent_obs global_obs) eqn:Hcase_biv.
+* (* Bivalent cases *)
+  assert (Hperm : PermutationA equiv (cons (get_location (config (Good g)))
+                             (cons (find_other_loc (fst global_obs) (get_location (config (Good g)))) nil))
+                             (cons (loc_g1 config) (cons (loc_others config) nil))).
+  { rewrite <- have_support. apply NoDupA_inclA_length_PermutationA; auto.
+    + repeat constructor; [rewrite InA_singleton | now rewrite InA_nil].
+      intro Habs. symmetry in Habs. revert Habs.
+      apply find_other_loc_diff, pos_in_config; auto.
+    + intros pt Hpt. rewrite InA_cons, InA_singleton in Hpt.
+      destruct Hpt as [Hpt | Hpt]; rewrite Hpt.
+      - rewrite support_spec. apply pos_in_config.
+      - rewrite support_spec. apply find_other_loc_In; auto. apply pos_in_config.
+    + rewrite have_support; auto. rewrite <- bivalent_obs_spec. apply Hcase_biv.
+    + rewrite <- bivalent_obs_spec. apply Hcase_biv. }
+  destruct (color_bivalent_obs global_obs) eqn:Hcase_col_biv;
+  [destruct (observer_lght (snd global_obs)) eqn:Hcase_light |].
+  + (* color bivalent and white observer *)
+    split; try reflexivity; [].
+    cbn -[equiv middle inverse loc_g1].
+    transitivity (middle (sim ⁻¹ 0%VS) (sim ⁻¹ (find_other_loc (fst local_obs) 0%VS))).
+    - now rewrite R2_middle_morph.
+    - change ((sim ⁻¹) 0%VS) with (center (change_frame da config g)).
+      rewrite similarity_center.
+      rewrite Hcenter, Hobs. cbn [fst]. rewrite find_other_loc_morph.
+      match goal with |- context[Bijection.section (sim_f (sim ⁻¹)) (Bijection.section (sim_f sim) ?x)] =>
+        change (Bijection.section (sim_f (sim ⁻¹)) (Bijection.section (sim_f sim) ?x)) with ((sim ⁻¹ ∘ sim) x) end.
+      rewrite (compose_inverse_l sim _). cbn [sim_f id Bijection.id Bijection.section].
+      rewrite PermutationA_2 in Hperm; auto.
+      destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]];
+      rewrite <- Heq1, <- Heq2; auto using middle_comm.
+  + (* color bivalent and black observer *)
+    rewrite Hcenter. split; try reflexivity; [].
+    apply Bijection.retraction_section.
+  + (* bivalent but not color bivalent *)
+    split; try reflexivity; []. cbn -[equiv inverse loc_g1].
+    transitivity (find_max_black (map (sim ⁻¹) (fst local_obs), map_light (sim ⁻¹) (snd local_obs))
+                                 ((sim ⁻¹) 0%VS) ((sim ⁻¹) (find_other_loc (fst local_obs) 0%VS))).
+    { symmetry. apply find_max_black_morph. }
+    transitivity (find_max_black global_obs (get_location (config (Good g))) (find_other_loc (fst global_obs) (get_location (config (Good g))))).
+    2:{ apply PermutationA_2 in Hperm; auto.
+        destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite <- Heq1, <- Heq2; auto.
+        apply find_max_black_comm.
+        - rewrite <- bivalent_obs_spec. apply Hcase_biv.
+        - rewrite <- color_bivalent_obs_spec, not_true_iff_false.
+          apply Hcase_col_biv.
+        - apply pos_in_config.
+        - apply find_other_loc_In, pos_in_config; auto. }
+    f_equiv.
+    - split; cbn -[equiv].
+      -- rewrite Hobs. cbn -[equiv]. rewrite map_merge; autoclass; [].
+         setoid_rewrite <- map_id at 3.
+         apply map_extensionality_compat; try (now repeat intro); [].
+         apply Bijection.retraction_section.
+      -- (* FIXME: rewrite Hobs fails here *)
+         transitivity (map_light (Bijection.retraction sim)
+                         (snd (map new_frame (fst global_obs), map_light new_frame (snd global_obs)))).
+         { now apply map_light_compat, snd_compat_pactole. }
+         cbn [snd]. rewrite map_light_merge; trivial.
+         transitivity (map_light id (snd global_obs)); [| now apply map_light_id].
+         apply map_light_extensionality_compat; try (now repeat intro); [].
+         apply Bijection.retraction_section.
     - apply (similarity_center da).
+    - (* TODO: perform the rewrite in the other direction *)
+      rewrite <- find_other_loc_morph. f_equiv.
+      -- rewrite Hobs. cbn [fst]. rewrite map_merge; auto; [].
+         setoid_rewrite <- map_id at 3. apply map_extensionality_compat; [now autoclass |].
+         apply Bijection.retraction_section.
+      -- apply (similarity_center da).
 * (* not bivalent *)
   unfold gatherR2_old_pgm.
   assert (supp_nonempty := support_non_nil config).
@@ -2295,279 +2746,91 @@ destruct (bivalent_obs global_obs) eqn:Hcase_biv;
       split; reflexivity.
     - (* Dirty case & not on SECT *)
       rewrite Hobs. cbn -[equiv].
-      rewrite target_morph, Bijection.retraction_section; trivial; [].
-      reflexivity.
-Qed.
-
-(** Since colors are not modified outside the color_bivalent case, changing robots are always moving. *)
-Lemma changing_eq_moving : forall config, ~color_bivalent config ->
-  changing gatherR2 da config = moving gatherR2 da config.
-Proof using Hssync.
-intros config Hcolor.
-unfold moving, changing.
-induction names as [| id l]; cbn -[equiv_dec get_location]; trivial; [].
-repeat destruct_match.
-+ apply IHl.
-+ revert_one equiv. intro Heq. rewrite Heq in *. intuition.
-+ exfalso. revert_one @complement. intro Habs. apply Habs. clear Habs.
-  split; trivial; [].
-  rewrite (round_simplify config id).
-  destruct_match; try reflexivity; [].
-  cbn zeta. destruct_match.
-  - rewrite <- (color_bivalent_obs_spec config (config id)), not_true_iff_false in Hcolor.
-    changeR2. rewrite Hcolor. cbn. changeR2. apply observer_light_get_light.
-  - now repeat destruct_match.
-+ f_equal. apply IHl.
-Qed.
-
-Corollary no_moving_same_config : forall config, ~color_bivalent config ->
-  moving gatherR2 da config = [] -> round gatherR2 da config == config.
-Proof using Hssync.
-intros ? ?.
-rewrite <- changing_eq_moving; trivial; [].
-apply no_changing_same_config.
-Qed.
-
-
-Lemma gathered_at_MajTower_at_iff : forall config l, gathered_at l config -> MajTower_at l config.
-Proof using size_G.
-  intros cfg l H. 
-  red in H.
-  red.
-  assert ((!! cfg)[l] > 0).
-  { assert (get_location (cfg (Good g1)) == l) by auto.
-    enough (In l (!! cfg)).
-    { auto. }
-    rewrite obs_from_config_In.
-    exists (Good g1);auto. }
-  intros y H1. 
-  assert ((!! cfg)[y] = 0).
-  { destruct ((!! cfg)[y]) eqn:heq.
-    { reflexivity. }
-    
-    assert ((!! cfg)[y] > 0) as hneq by lia.
-    assert (In y (!! cfg)) as hIn.
-    { red. 
-      assumption. }
-    rewrite obs_from_config_In in hIn.
-    exfalso.
-    destruct hIn. 
-    revert H2.
-    pattern x.
-    apply no_byz.
-    intros g H2. 
-    rewrite H in H2.
-    symmetry in H2.
-    contradiction. }
-  lia.
-Qed.
-
-Definition light_on l pt config :=
-  List.filter (fun id => get_light (config id) ==b l) (on_loc pt config).
-Notation black_on := (light_on false).
-Notation white_on := (light_on true).
-
-Lemma length_light_on : forall l pt config,
-  length (light_on l pt config) = (colors (snd (!!! (config, (0%VS, witness)))))[(pt, l)].
-Proof using .
-intros l pt config. destruct (obs_from_config_spec config (0%VS, witness)) as [_ [_ Hobs]].
-rewrite Hobs, config_list_spec, count_filter_length, filter_map, map_length.
-unfold black_on, on_loc. rewrite <- filter_andb. f_equal. f_equiv.
-intros xx id ?. subst xx. clear.
-symmetry. destruct_match; symmetry.
-- revert_one @equiv. intros [Heq1 Heq2]. unfold get_light. simpl get_location.
-  rewrite Heq1, Heq2. now simpl_bool.
-- reflect_bool. destruct (get_light (config id) =?= l); firstorder.
-Qed.
-
-Lemma bivalent_In_iff_mult_eq_half : forall config, bivalent config ->
-  forall pt, In pt (!! config) <-> (!! config)[pt] = Nat.div2 (nG + nB).
-Proof using size_G.
-intros config Hbivalent pt. split; intro Hin.
-+ rewrite <- support_spec in Hin.
-  apply extend_bivalent in Hbivalent.
-  destruct Hbivalent as [_ [_ [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 [Hsupp [Hin_supp Hother]]]]]]]]].
-  changeR2. rewrite Hsupp, InA_cons, InA_singleton in Hin.
-  destruct Hin as [Heq | Heq]; rewrite Heq; auto.
-+ unfold In. rewrite Hin. auto.
-Qed.
-
-
-Section ColorBivalent.
-
-Variable config : configuration.
-Hypothesis Hcolor : color_bivalent config.
-
-Definition loc_g1 := get_location (config (Good g1)).
-Definition loc_others := find_other_loc (!!config) loc_g1.
-
-
-(* Some trivial lemmas that are overused *)
-Local Lemma have_bivalent_obs : bivalent_obs (!!! (config, (0%VS, witness))) = true.
-Proof using Hcolor. now apply bivalent_obs_spec, color_bivalent_bivalent. Qed.
-
-Local Definition loc_g1_In : In loc_g1 (!! config) := pos_in_config _ _ _.
-Local Definition loc_g1_In_fst : forall st, In loc_g1 (fst (!!! (config, st))) := fun st => pos_in_config _ st _.
-
-Local Lemma loc_others_In : In loc_others (!! config).
-Proof using Hcolor.
-rewrite <- support_spec, obs_fst, find_other_loc_spec.
-- now right; left.
-- apply have_bivalent_obs.
-- apply pos_in_config.
-Qed.
-
-Local Lemma loc_others_In_fst : forall st, In loc_others (fst (!!! (config, st))).
-Proof using Hcolor. intro. apply loc_others_In. Qed.
-
-Local Lemma In_fst_config : forall id, In (get_location (config id)) (fst (!!! (config, (0%VS, witness)))).
-Proof using . intro id. apply pos_in_config. Qed.
-
-Local Lemma loc_g1_diff_others: loc_g1 =/= loc_others.
-Proof using Hcolor.
-  unfold loc_others.
-  symmetry.
-  rewrite obs_fst with (st:=(origin,witness)).
-  apply find_other_loc_diff.
-  - now apply bivalent_obs_spec, color_bivalent_bivalent.
-  - apply pos_in_config.
-Qed.
-
-Local Lemma find_other_loc_diff_here : find_other_loc (!! config) loc_g1 =/= loc_g1.
-Proof using Hcolor.
-rewrite obs_fst. apply find_other_loc_diff.
-- apply have_bivalent_obs.
-- apply loc_g1_In_fst.
-Qed.
-
-Local Lemma other_than_loc_g1 : forall id, get_location (config id) =/= loc_g1 -> get_location (config id) == loc_others.
-Proof using Hcolor.
-intros.
-eapply (bivalent_same_location (0%VS, witness) (color_bivalent_bivalent Hcolor) (pt3 := loc_g1)).
-- apply pos_in_config.
-- apply loc_others_In_fst.
-- apply pos_in_config.
-- assumption.
-- symmetry. apply loc_g1_diff_others.
-Qed.
-
-Local Lemma other_than_loc_others : forall id, get_location (config id) =/= loc_others -> get_location (config id) == loc_g1.
-Proof using Hcolor.
-intros.
-eapply (bivalent_same_location (0%VS, witness) (color_bivalent_bivalent Hcolor) (pt3 := loc_others)).
-- apply pos_in_config.
-- apply pos_in_config.
-- apply loc_others_In_fst.
-- assumption.
-- apply loc_g1_diff_others.
-Qed.
-
-Local Lemma have_support : PermutationA equiv (support (!! (config))) (cons loc_g1 (cons loc_others nil)).
-Proof using Hcolor.
-rewrite obs_fst.
-apply find_other_loc_spec.
-- apply have_bivalent_obs.
-- apply loc_g1_In_fst.
-Qed.
-
-Local Lemma loc_g1_mult : (!! config)[loc_g1] = Nat.div2 (nG + nB).
-Proof using Hcolor.
-apply color_bivalent_bivalent in Hcolor.
-apply extend_bivalent in Hcolor.
-destruct Hcolor as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 [_ [Hin _]]]]]]]]].
-changeR2. specialize (Hin _ loc_g1_In).
-now destruct Hin as [Heq | Heq]; rewrite Heq.
+      rewrite target_morph, Bijection.retraction_section; trivial; [].
+      reflexivity.
 Qed.
 
-Local Lemma loc_others_mult : (!! config)[loc_others] = Nat.div2 (nG + nB).
-Proof using Hcolor.
-assert (Hbivalent := color_bivalent_bivalent Hcolor).
-apply extend_bivalent in Hbivalent.
-destruct Hbivalent as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 [_ [Hin _]]]]]]]]].
-changeR2. specialize (Hin _ loc_others_In).
-now destruct Hin as [Heq | Heq]; rewrite Heq.
+(** Since colors are not modified outside the color_bivalent case, changing robots are always moving. *)
+Lemma changing_eq_moving : forall config, ~color_bivalent config ->
+  changing gatherR2 da config = moving gatherR2 da config.
+Proof using Hssync.
+intros config Hcolor.
+unfold moving, changing.
+induction names as [| id l]; cbn -[equiv_dec get_location]; trivial; [].
+repeat destruct_match.
++ apply IHl.
++ revert_one equiv. intro Heq. rewrite Heq in *. intuition.
++ exfalso. revert_one @complement. intro Habs. apply Habs. clear Habs.
+  split; trivial; [].
+  rewrite (round_simplify config id).
+  destruct_match; try reflexivity; [].
+  cbn zeta. destruct_match.
+  - rewrite <- (color_bivalent_obs_spec config (config id)), not_true_iff_false in Hcolor.
+    changeR2. rewrite Hcolor. cbn. changeR2. apply observer_light_get_light.
+  - now repeat destruct_match.
++ f_equal. apply IHl.
 Qed.
 
-Hint Immediate pos_in_config have_bivalent_obs loc_g1_In loc_g1_In_fst loc_others_In loc_others_In_fst
-               In_fst_config find_other_loc_diff_here loc_g1_mult loc_others_mult : core.
-Hint Resolve other_than_loc_g1 other_than_loc_others mult_div2_In color_bivalent_bivalent : core.
-
-Lemma loc_g1_or_loc_others_eqb : forall id,
-  get_location (config id) ==b loc_others = negb (get_location (config id) ==b loc_g1).
-Proof using Hcolor.
-intro id. unfold loc_others.
-destruct (get_location (config id) ==b loc_g1) eqn:Hcase; cbn [negb]; reflect_bool.
-+ rewrite Hcase, (obs_fst (0%VS, witness)).
-  symmetry. apply find_other_loc_diff; auto.
-+ apply (bivalent_same_location (0%VS, witness) (color_bivalent_bivalent Hcolor) (pt3 := loc_g1)); auto.
+Corollary no_moving_same_config : forall config, ~color_bivalent config ->
+  moving gatherR2 da config = [] -> round gatherR2 da config == config.
+Proof using Hssync.
+intros ? ?.
+rewrite <- changing_eq_moving; trivial; [].
+apply no_changing_same_config.
 Qed.
 
 
-(* We find a robot not on the same location as g1 *)
-Definition find_other_id :=
-  List.find (fun id => if (get_location (config id) =?= (get_location (config (Good g1)))) then false else true) names.
-
-Lemma ex_other: { id | get_location (config id) =/= get_location (config (Good g1))}.
-Proof using Hcolor.
-  destruct find_other_id eqn:heq.
-  - exists i;auto.
-    unfold find_other_id in *.
-    destruct (find_some _ _ heq).
-    destruct (get_location (config i) =?= get_location (config (Good g1)));auto;discriminate.
-  - exfalso.
-    unfold find_other_id in *.
-    specialize  (find_none _ _ heq) as h.
-    cbn -[names equiv_dec get_location] in h.
-
-    assert (gathered_at (get_location (config (Good g1))) config).
-    { red.
-      intros g. 
-      specialize (h (Good g) (In_names _)).
-      changeR2.
-      destruct (get_location (config (Good g)) =?= get_location (config (Good g1)));auto. }
-    assert (MajTower_at (get_location (config (Good g1))) config).
-    { now apply gathered_at_MajTower_at_iff. }
-
-    destruct (Majority_not_bivalent H0).
-    now apply color_bivalent_bivalent.
+Lemma gathered_at_MajTower_at_iff : forall config l, gathered_at l config -> MajTower_at l config.
+Proof using size_G.
+  intros cfg l H. 
+  red in H.
+  red.
+  assert ((!! cfg)[l] > 0).
+  { assert (get_location (cfg (Good g1)) == l) by auto.
+    enough (In l (!! cfg)).
+    { auto. }
+    rewrite obs_from_config_In.
+    exists (Good g1);auto. }
+  intros y H1. 
+  assert ((!! cfg)[y] = 0).
+  { destruct ((!! cfg)[y]) eqn:heq.
+    { reflexivity. }
+    
+    assert ((!! cfg)[y] > 0) as hneq by lia.
+    assert (In y (!! cfg)) as hIn.
+    { red. 
+      assumption. }
+    rewrite obs_from_config_In in hIn.
+    exfalso.
+    destruct hIn. 
+    revert H2.
+    pattern x.
+    apply no_byz.
+    intros g H2. 
+    rewrite H in H2.
+    symmetry in H2.
+    contradiction. }
+  lia.
 Qed.
 
-Definition g2:ident.
-Proof.
-  destruct ex_other as [ x _ ].
-  exact x.
-Defined.
 
-Lemma g2_spec:  get_location (config g2) =/= get_location (config (Good g1)).
-Proof.
-  unfold g2.
-  destruct ex_other.
-  assumption.
-Qed.
+Section ColorBivalent.
 
-(* Robots partitionned wrt to their location, activation and color. *)
-Definition active_on pt config :=
-  List.filter (fun id => equiv_decb (get_location (config id)) pt) (active da).
+Variable config : configuration.
+Hypothesis Hcolor : color_bivalent config.
+
+Notation loc_g1 := (loc_g1 config).
+Notation loc_others := (loc_others config).
 Notation active_on_g1 := (active_on loc_g1 config).
 Notation active_on_other := (active_on loc_others config).
-Definition idle_on pt config :=
-  List.filter (fun id => equiv_decb (get_location (config id)) pt) (idle da).
 Notation idle_on_g1 := (idle_on loc_g1 config).
 Notation idle_on_other := (idle_on loc_others config).
-Definition light_active_on l pt config :=
-  List.filter (fun id => get_light (config id) ==b l) (active_on pt config).
-Notation black_active_on := (light_active_on false).
 Notation black_active_on_g1 := (black_active_on loc_g1 config).
 Notation black_active_on_other := (black_active_on loc_others config).
-Notation white_active_on := (light_active_on true).
 Notation white_active_on_g1 := (white_active_on loc_g1 config).
 Notation white_active_on_other := (white_active_on loc_others config).
-Definition light_idle_on l pt config :=
-  List.filter (fun id => get_light (config id) ==b l) (idle_on pt config).
-Notation black_idle_on := (light_idle_on false).
 Notation black_idle_on_g1 := (black_idle_on loc_g1 config).
 Notation black_idle_on_other := (black_idle_on loc_others config).
-Notation white_idle_on := (light_idle_on true).
 Notation white_idle_on_g1 := (white_idle_on loc_g1 config).
 Notation white_idle_on_other := (white_idle_on loc_others config).
 Notation black_on_g1 := (black_on loc_g1 config).
@@ -2576,110 +2839,146 @@ Notation white_on_g1 := (white_on loc_g1 config).
 Notation white_on_other := (white_on loc_others config).
 
 
-Definition active_partition :=
-  List.partition (fun id => equiv_decb (get_location (config id)) loc_g1) (active da).
-
-Lemma active_partition_spec : active_partition = (active_on_g1, active_on_other).
-Proof using Hcolor.
-unfold active_on, active_partition.
-rewrite partition_filter. f_equal.
-rewrite <- eqlistA_Leibniz.
-apply filter_extensionalityA_compat; try reflexivity; [].
-intros xx id ?. subst xx. unfold loc_others. symmetry.
-destruct (get_location (config id) ==b loc_g1) eqn:Hcase; reflect_bool.
-* rewrite Hcase. symmetry. apply find_other_loc_diff_here.
-* eapply (bivalent_same_location (0%VS, witness) (color_bivalent_bivalent Hcolor) (pt3 := loc_g1)); auto.
-Qed.
-
-Lemma active_split : PermutationA equiv (active_on_g1 ++ active_on_other) (active da).
+Lemma color_bivalent_length_black :
+  length (black_on loc_g1 config) = length (black_on loc_others config).
 Proof using Hcolor.
-  replace active_on_g1 with (fst active_partition).
-  replace active_on_other with (snd active_partition).
-  { apply partition_PermutationA. }
-  { now rewrite active_partition_spec. }
-  { now rewrite active_partition_spec. }
+assert (Hblack : List.In false l_list) by now right; left.
+destruct Hcolor as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 Hcol]]]]]]].
+rewrite Forall_forall in Hcol. apply Hcol in Hblack. clear Hcol.
+rewrite <- 2 length_light_on in Hblack.
+assert (Hperm : PermutationA equiv (support (!! config)) (cons pt1 (cons pt2 nil))).
+{ rewrite obs_fst. changeR2. apply bivalent_support; auto. }
+rewrite have_support in Hperm; auto; [].
+apply PermutationA_2 in Hperm; auto; [].
+destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; now rewrite Heq1, Heq2.
 Qed.
 
-Lemma idle_split: PermutationA equiv (idle da) (idle_on_g1 ++ idle_on_other).
+Lemma color_bivalent_length_white :
+  length (white_on loc_g1 config) = length (white_on loc_others config).
 Proof using Hcolor.
-unfold idle_on.
-induction (idle da); cbn [List.filter]; try reflexivity; [].
-rewrite loc_g1_or_loc_others_eqb.
-changeR2. destruct_match; cbn [negb app].
-- now constructor.
-- rewrite <- PermutationA_middle; autoclass.
-  now constructor.
-Qed.
-
-Lemma active_on_split : forall pt config,
-  PermutationA equiv (active_on pt config) (black_active_on pt config ++ white_active_on pt config).
-Proof using .
-clear config Hcolor.
-intros pt config. unfold black_active_on, white_active_on.
-induction (active_on pt) as [| id l]; cbn [List.filter]; try reflexivity; [].
-do 2 destruct_match; cbn [app].
-- reflect_bool. congruence.
-- now constructor.
-- rewrite <- PermutationA_middle; autoclass.
-  now constructor.
-- exfalso. destruct (get_light (config id)); cbn in *; discriminate.
+assert (Hall : length (on_loc loc_g1 config) = length (on_loc loc_others config)).
+{ rewrite <- 2 (obs_from_config_on_loc config (0%VS, witness)), loc_g1_mult, loc_others_mult; auto. }
+rewrite 2 on_loc_color_split, 2 app_length, color_bivalent_length_black in Hall.
+lia.
 Qed.
 
-Lemma idle_on_split : forall pt config,
-  PermutationA equiv (idle_on pt config) (black_idle_on pt config ++ white_idle_on pt config).
+Definition ofc := @obs_from_config.
+Lemma obs_fst_colors : forall pt l,
+  (colors (snd (!!! (config, (0%VS, witness)))))[(pt, l)] <= (!! config)[pt].
 Proof using .
-clear config Hcolor.
-intros pt config. unfold black_idle_on, white_idle_on.
-induction (idle_on pt) as [| id l]; cbn [List.filter]; try reflexivity; [].
-do 2 destruct_match; cbn [app].
-- reflect_bool. congruence.
-- now constructor.
-- rewrite <- PermutationA_middle; autoclass.
-  now constructor.
-- exfalso. destruct (get_light (config id)); cbn in *; discriminate.
+intros pt l. rewrite obs_fst.
+destruct (Obs.(obs_from_config_spec) config (0%VS, witness)) as [Hobs_fst [Hlight Hcolors]].
+rewrite Hobs_fst, Hcolors.
+clear Hcolors Hlight Hobs_fst. changeR2.
+induction (config_list config) as [| [pt' l'] config_list].
++ reflexivity.
++ cbn -[equiv_dec equiv get_location].
+  repeat destruct_match.
+  - apply le_n_S, IHconfig_list.
+  - exfalso. revert_one @complement. intro Habs. apply Habs.
+    revert_all. now intros [].
+  - apply le_S, IHconfig_list.
+  - apply IHconfig_list.
+Qed.
+
+Definition ref_colors := let nb_loc_g1_black := length (black_on loc_g1 config) in
+                         add (loc_g1,     false) nb_loc_g1_black
+                        (add (loc_g1,     true) (Nat.div2 (nG + nB) - nb_loc_g1_black)
+                        (add (loc_others, false) nb_loc_g1_black
+                  (singleton (loc_others, true) (Nat.div2 (nG + nB) - nb_loc_g1_black)))).
+
+Lemma have_obs : forall st,
+  !!! (config, st) == ((add loc_g1 (Nat.div2 (nG + nB)) (singleton loc_others (Nat.div2 (nG + nB)))),
+                       {| observer_lght := get_light st; colors := ref_colors |}).
+Proof using Hcolor.
+intros st.
+unfold ref_colors.
+split; [| split].
+* rewrite <- (obs_from_config_fst_ok (0%VS, witness) st). cbn [fst]. changeR2.
+  intro pt.
+  destruct (pt =?= loc_g1) as [Hpt | Hloc_g1];
+  [| destruct (pt =?= loc_others) as [Hpt | Hloc_others]].
+  + rewrite Hpt, add_same, singleton_other; auto.
+  + rewrite Hpt, add_other, singleton_same; auto.
+  + rewrite add_other, singleton_other; auto; [].
+    rewrite <- not_In, <- support_spec, have_support, InA_cons, InA_singleton; auto.
+    intuition.
+* intros [pt l]. cbn [snd colors].
+  assert (Heq : length (on_loc pt config) = length (white_on pt config) + length (black_on pt config)).
+  { rewrite on_loc_color_split, app_length. lia. }
+  rewrite <- (obs_from_config_on_loc config (0%VS, witness)) in Heq.
+  rewrite colors_indep, <- length_light_on.
+  destruct (pt =?= loc_g1) as [Hpt | Hloc_g1];
+  [| destruct (pt =?= loc_others) as [Hpt | Hloc_others]].
+  1,2: destruct l.
+  + (* white on loc_g1 *)
+    rewrite Hpt in *.
+    rewrite loc_g1_mult in *; auto.
+    rewrite add_other, add_same, add_other, singleton_other.
+    - lia.
+    - intros [Hfst Hsnd]. cbn -[equiv get_location] in Hfst, Hsnd.
+      apply loc_g1_diff_others in Hfst; auto.
+    - intros []. intuition.
+    - intros []. intuition.
+  + (* black on loc_g1 *)
+    rewrite Hpt in *.
+    rewrite add_same, add_other, add_other, singleton_other.
+    - lia.
+    - intros []. intuition.
+    - intros []. clear Heq. cbn -[equiv get_location] in *.
+      apply loc_g1_diff_others in H; auto.
+    - intros []. intuition.
+  + (* white on loc_others *)
+    rewrite Hpt in *.
+    rewrite loc_others_mult, <- color_bivalent_length_black in *; auto.
+    rewrite 3 add_other, singleton_same.
+    - lia.
+    - intros []. intuition.
+    - intros []. intuition.
+    - intros []. intuition.
+  + (* black on loc_others *)
+    rewrite Hpt in *.
+    rewrite loc_others_mult, <- color_bivalent_length_black in *; auto.
+    rewrite 2 add_other, add_same, singleton_other.
+    - lia.
+    - intros []. intuition.
+    - intros []. intuition.
+    - intros []. intuition.
+  + (* on empty locations *)
+    rewrite 3 add_other, singleton_other.
+    - rewrite length_light_on, <- Nat.le_0_r, obs_fst_colors, Nat.le_0_r, <- not_In.
+      rewrite <- support_spec, have_support, InA_cons, InA_singleton; auto.
+      intuition.
+    - intros []. intuition.
+    - intros []. intuition.
+    - intros []. intuition.
+    - intros []. intuition.
+* cbn. reflexivity.
 Qed.
 
-Lemma on_loc_split : forall pt config,
-  PermutationA equiv (on_loc pt config) (active_on pt config ++ idle_on pt config).
-Proof.
-clear config Hcolor.
-intros pt config. symmetry.
-unfold on_loc, active_on, active, idle_on, idle.
-induction names as [| id l]; cbn [List.filter]; try reflexivity; [].
-do 2 (destruct_match; cbn [app List.filter negb]).
-- now constructor.
-- apply IHl.
-- rewrite <- PermutationA_middle; autoclass.
-  now constructor.
-- apply IHl.
-Qed.
+Corollary have_colors : forall st, colors (snd (!!! (config, st))) == ref_colors.
+Proof using Hcolor. intro st. now rewrite have_obs. Qed.
 
-Lemma on_loc_color_split : forall pt config,
-  PermutationA equiv (on_loc pt config) (black_on pt config ++ white_on pt config).
-Proof.
-clear config Hcolor.
-intros pt config.
-unfold light_on, on_loc.
-induction names as [| id l]; cbn [List.filter]; try reflexivity; [].
-repeat (destruct_match; cbn [app List.filter]); reflect_bool.
-- congruence.
-- now constructor.
-- rewrite <- PermutationA_middle; autoclass.
-  now constructor.
-- destruct (get_light (config id)); intuition.
-- assumption.
+Lemma same_colors : forall col, (colors (snd (!!! (config, (0%VS, witness)))))[(loc_g1, col)] =
+                                (colors (snd (!!! (config, (0%VS, witness)))))[(loc_others, col)].
+Proof using Hcolor.
+intro col. rewrite have_colors. unfold ref_colors.
+assert (loc_g1 =/= loc_others) by auto. unfold complement in *.
+destruct col.
++ rewrite add_other, add_same, 4 add_other, singleton_other, singleton_same;
+  reflexivity || intros []; cbn in *; intuition.
++ rewrite add_same, 4 add_other, add_same, 2 singleton_other;
+  reflexivity || intros []; cbn in *; intuition.
 Qed.
 
-
 Theorem round_simplify_color_bivalent :
   round gatherR2 da config
   == fun id =>
      if da.(activate) id
      then
        let obs := !!!(config, config id) in
-       let other_loc := find_other_loc (fst obs) (get_location (config id)) in
        if observer_lght (snd obs)
-       then (middle (get_location (config id)) other_loc, false)
+       then (middle loc_g1 loc_others, false)
        else (get_location (config id), true) (* was: (other_loc, true) *)
      else config id.
 Proof using Hssync Hcolor.
@@ -2700,21 +2999,15 @@ Proof using Hssync Hcolor.
   rewrite moving_spec, active_spec, (round_simplify_color_bivalent id).
   split.
   - cbn zeta.
-    repeat destruct_match;intuition.
+    repeat destruct_match; intuition.
   - intros [h_white h_active].
     rewrite h_active.
     cbn zeta.
     setoid_rewrite observer_light_get_light. rewrite h_white.
-    assert (Hperm : PermutationA equiv (support (fst (!!! (config, config id))))
-      (get_location (config id) :: find_other_loc (fst (!!! (config, config id))) (get_location (config id)) :: nil)).
-    { apply find_other_loc_spec.
-      - rewrite bivalent_obs_spec. now apply color_bivalent_bivalent.
-      - apply pos_in_config. }
-    assert (Hnodup := support_NoDupA (fst (!!! (config, config id)))).
-    rewrite Hperm in Hnodup. inv Hnodup. revert_one not. rewrite InA_singleton.
-    intro Hneq. apply middle_diff in Hneq.
-    rewrite InA_cons, InA_singleton in Hneq.
-    intro Habs. apply Hneq. now left.
+    unfold get_location at 1. cbn -[middle equiv get_location].
+    assert (Hdiff := middle_diff (@loc_g1_diff_others config ltac:(auto))).
+    rewrite InA_cons, InA_singleton in Hdiff.
+    destruct (@bivalent_get_location_cases config ltac:(auto) id) as [Heq | Heq]; rewrite Heq; intuition.
 Qed.
 
 Lemma color_bivalent_moving_target : forall id, List.In id (moving gatherR2 da config) ->
@@ -2726,17 +3019,7 @@ rewrite moving_iff, active_spec in Hid.
 unfold is_white in Hid.
 destruct Hid as [Hwhite Hactive].
 cbn zeta.
-rewrite Hactive, (observer_light_get_light config), Hwhite.
-assert (Hperm : PermutationA equiv (support (fst (!!! (config, config id))))
-  (cons (get_location (config id))
-    (cons (find_other_loc (fst (!!! (config, config id))) (get_location (config id))) nil))).
-{ apply find_other_loc_spec; auto. }
-rewrite have_support in Hperm.
-symmetry in Hperm.
-apply PermutationA_2 in Hperm; auto; [].
-destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite Heq2, Heq1.
-- reflexivity.
-- now rewrite middle_comm.
+now rewrite Hactive, (observer_light_get_light config), Hwhite.
 Qed.
 
 Lemma color_bivalent_same_destination : same_destination_if_moving gatherR2 da config.
@@ -2834,9 +3117,9 @@ Corollary a3b_state_same_eqb : forall id,
 Proof using Hssync Hcolor Hallblack. intro. rewrite state_eqb, a3b_same_loc. now simpl_bool. Qed.
 
 Lemma a3b_black_active_is_active : forall pt,
-  List.filter (fun id => get_light (config id) ==b false) (active_on pt config) = active_on pt config.
-Proof.
-intro pt. unfold active_on, active.
+  black_active_on pt config = active_on pt config.
+Proof using Hallblack.
+intro pt. unfold light_active_on, active_on, active.
 repeat rewrite <- filter_andb. f_equiv.
 intros xx id ?. subst xx.
 unfold all_active_are_black, all_are_black_in in *. rewrite Forall_forall in *.
@@ -2855,6 +3138,33 @@ rewrite a3b_next_black_eqb, a3b_same_loc.
 now destruct (activate da id); simpl_bool.
 Qed.
 
+Lemma a3b_next_black_is_black_idle :forall pt,
+  black_on pt (round gatherR2 da config) = black_idle_on pt config.
+Proof using Hssync Hcolor Hallblack.
+intro pt.
+unfold black_idle_on, black_on, idle_on, idle, on_loc.
+repeat rewrite <- filter_andb.
+induction names as [| id l]; try reflexivity; [].
+cbn [List.filter].
+rewrite (a3b_same_loc id).
+rewrite all_active_are_black_equiv in Hallblack.
+destruct_match_eq Htest1; destruct_match_eq Htest2; reflect_bool.
++ now f_equal.
++ exfalso.
+  destruct Htest1 as [Hlight' Hloc].
+  revert Hlight'. rewrite (round_simplify_color_bivalent id).
+  cbn zeta. setoid_rewrite (observer_light_get_light config id).
+  destruct_match_eq Hactive; try destruct_match_eq Hlight.
+  - apply Hallblack in Hactive. unfold is_black in *. congruence.
+  - discriminate.
+  - intuition.
++ exfalso.
+  destruct Htest2 as [[Hlight Hloc] Hactive].
+  destruct Htest1 as [Htest1 | Htest1]; try congruence; [].
+  rewrite (round_simplify_color_bivalent id), Hactive in Htest1. congruence.
++ apply IHl.
+Qed.
+
 Lemma a3b_white_idle_is_white : forall pt, white_idle_on pt config = white_on pt config.
 Proof using Hallblack.
 intros pt. unfold light_idle_on, idle_on, idle, white_on, on_loc.
@@ -2893,7 +3203,7 @@ destruct_match; auto; [].
 exfalso. reflect_bool. intuition congruence.
 Qed.
 
-Lemma a3b_length_black_idle : forall pt pt',
+Lemma a3b_length_black_idle_eq : forall pt pt',
   length (List.filter (fun id => (config id ==b (pt, false)) && negb (activate da id)) (black_idle_on pt' config))
   = if pt' ==b pt then length (black_idle_on pt' config) else 0.
 Proof using .
@@ -2913,8 +3223,9 @@ destruct (pt' ==b pt) eqn:Heq_pt.
 Qed.
 
 Lemma a3b_length_white_idle : forall pt pt',
-  length (List.filter (fun id => (config id ==b (pt, false)) && negb (activate da id)) (white_idle_on pt' config)) = 0.
-Proof.
+  length (List.filter (fun id => (config id ==b (pt, false))
+                                 && negb (activate da id)) (white_idle_on pt' config)) = 0.
+Proof using .
 intros pt pt'. unfold white_idle_on. rewrite <- filter_andb.
 induction (idle_on pt'); cbn; try reflexivity; [].
 destruct_match; auto; [].
@@ -2954,26 +3265,18 @@ Lemma color_bivalent_next_color_bivalent :
   color_bivalent (round gatherR2 da config).
 Proof using Hssync Hcolor.
 intros [Hactive Hlen].
-assert (Hcol := Hcolor). destruct Hcol as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 Hall]]]]]]].
-assert (Hlen' : length (active_on pt1 config) = length (active_on pt2 config)).
-{ assert (Hperm : PermutationA equiv (support (!! config)) (cons pt1 (cons pt2 nil))).
-  { rewrite obs_fst. eapply (bivalent_support (color_bivalent_bivalent Hcolor)); auto. }
-  rewrite have_support in Hperm. apply PermutationA_2 in Hperm; autoclass; [].
-  destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite <- Heq1, <- Heq2; auto. }
-clear Hlen.
+assert (Hcol := Hcolor). destruct Hcol as [Heven [Hn _]].
 repeat split; trivial; [].
-exists pt1, pt2.
-repeat split.
-* assumption.
-* now rewrite a3b_same_obs.
-* now rewrite a3b_same_obs.
+exists loc_g1, loc_others.
+repeat split; auto; changeR2.
+* rewrite a3b_same_obs; auto.
+* rewrite a3b_same_obs; auto.
 * rewrite Forall_forall in *.
   intros col _.
-  assert (Hwhite : List.In true l_list) by now left.
-  assert (Hblack : List.In false l_list) by now right; left.
-  apply Hall in Hwhite, Hblack. clear Hall.
+  assert (Hwhite := color_bivalent_length_white).
+  assert (Hblack := color_bivalent_length_black).
   rewrite <- 2 length_light_on in *.
-  (* Splitting robots wrt. activation, color in the goal *)
+  (* Splitting robots wrt. activation, color in the goal: active (black), idle black, idle white  *)
   unfold light_on, on_loc.
   rewrite (active_idle_is_partition da).
   repeat rewrite filter_app.
@@ -2995,7 +3298,7 @@ repeat split.
                         (idle_on ?pt (round gatherR2 da config)))
       with (white_idle_on pt (round gatherR2 da config)).
     rewrite 2 (filter_extensionalityA_compat (Hfun (round gatherR2 da config) true) (reflexivity _)), 2 filter_false.
-    assert (Hlen : forall pt,
+    assert (Hlen' : forall pt,
               length (List.filter (fun id => get_light (round gatherR2 da config id) ==b true)
                         (active_on pt (round gatherR2 da config))) = length (active_on pt config)).
     { intro pt. unfold active_on, active.
@@ -3004,7 +3307,7 @@ repeat split.
       intros xx id ?. subst xx.
       rewrite a3b_next_white_eqb, a3b_same_loc; trivial; [].
       destruct (activate da id) eqn:Hid; now simpl_bool. }
-    rewrite 2 Hlen, 2 a3b_next_white_idle_is_white; trivial; [].
+    rewrite 2 Hlen', 2 a3b_next_white_idle_is_white; trivial; [].
     lia.
   + (* black *)
     rewrite 2 active_on_split.
@@ -3015,7 +3318,7 @@ repeat split.
                         (idle_on ?pt (round gatherR2 da config)))
       with (black_idle_on pt (round gatherR2 da config)).
     rewrite 2 (filter_extensionalityA_compat (Hfun (round gatherR2 da config) false) (reflexivity _)), 2 filter_false.
-    assert (Hlen : forall pt,
+    assert (Hlen' : forall pt,
               length (List.filter (fun id => get_light (round gatherR2 da config id) ==b false)
                                   (active_on pt (round gatherR2 da config))) = 0).
     { intro pt. unfold active_on, active.
@@ -3025,11 +3328,10 @@ repeat split.
       intros xx id ?. subst xx.
       rewrite a3b_next_black_eqb, a3b_same_loc; trivial; [].
       destruct (activate da id) eqn:Hid; now simpl_bool. }
-    rewrite 2 Hlen, 2 a3b_next_black_idle_is_black_idle; trivial; [].
-    assert (Heq : length (on_loc pt1 config) = length (on_loc pt2 config)).
-    { rewrite obs_from_config_on_loc in Hpt1, Hpt2. changeR2. congruence. }
-    rewrite 2 on_loc_split, 2 idle_on_split, 2 a3b_white_idle_is_white in Heq; trivial; [].
-    repeat rewrite ?filter_app, <- ?filter_andb, ?app_length in Heq.
+    rewrite 2 Hlen', 2 a3b_next_black_idle_is_black_idle; trivial; [].
+    assert (Heq : length (on_loc loc_g1 config) = length (on_loc loc_others config)).
+    { rewrite <- 2 (obs_from_config_on_loc _ (0%VS, witness)), loc_others_mult; auto. }
+    rewrite 2 on_loc_split_active_colors, 2a3b_white_idle_is_white, 4 app_length in Heq; auto.
     simpl. lia.
 Qed.
 
@@ -3064,35 +3366,36 @@ Lemma color_bivalent_next_bivalent_all_white :
   /\ ~color_bivalent (round gatherR2 da config).
 Proof using Hssync Hcolor.
 intros [Hall Hloc].
-assert (Hlen : length (active da) = Nat.div2 (nG + nB)).
+assert (Hlen_active : length (active da) = Nat.div2 (nG + nB)).
 { rewrite Hloc, <- (obs_from_config_on_loc config (0%VS, witness)).
-  rewrite <- bivalent_In_iff_mult_eq_half, obs_from_config_In.
+  rewrite <- bivalent_In_iff_mult_eq_half, obs_from_config_In; auto.
   destruct (active da) as [| id_active l].
   + exfalso. cut (List.In (Good g1) nil); intuition; [].
     now rewrite Hloc, on_loc_spec.
-  + now exists id_active.
-  + auto. }
-assert (Hidle : length (idle da) = Nat.div2 (nG + nB)).
+  + now exists id_active. }
+assert (Hlen_idle : length (idle da) = Nat.div2 (nG + nB)).
 { assert (Hlen' : length (idle da) + length (active da) = nG + nB).
   { rewrite <- names_length, (active_idle_is_partition da), app_length. lia. }
   destruct Hcolor as [Heven _]. apply even_div2 in Heven. lia. }
+assert (Nat.div2 (nG + nB) > 0) by auto.
+destruct (active da) as [| id_move l_active] eqn:Heq_active; [cbn in *; lia |].
+destruct (idle da) as [| id_inactive l_inactive] eqn:Heq_idle; [cbn in *; lia |].
+cbn [hd] in Hloc. rewrite <- Heq_active, <- Heq_idle in *.
+pose (pt1 := get_location (config id_move)).
+pose (pt2 := find_other_loc (fst (!!! (config, (0%VS, witness)))) pt1).
 assert (Hwhite : forall id, get_light (config id) == true).
 { intros id. unfold all_are_white, all_are_white_in in Hall.
   rewrite Forall_forall in Hall. apply Hall. apply In_names. }
 clear Hall.
 assert (Hbivalent : bivalent_obs (!!! (config, (0%VS, witness))) = true).
 { rewrite bivalent_obs_spec. now apply color_bivalent_bivalent. }
-assert (Hdiff : forall id, middle (get_location (config id))
-                  (find_other_loc (fst (!!! (config, config id))) (get_location (config id)))
-                =/= (get_location (config id))).
+assert (Hdiff : forall id, middle loc_g1 loc_others =/= (get_location (config id))).
 { intro id.
-  assert (Hdiff := pos_in_config config (origin, witness) id).
-  set (pt := get_location (config id)). fold pt in Hdiff.
-  set (pt' := find_other_loc (!! config) pt).
-  rewrite (obs_fst (origin, witness)) in Hdiff. changeR2.
-  apply find_other_loc_diff, middle_diff in Hdiff; trivial; [].
-  rewrite InA_cons, InA_singleton in Hdiff. apply Classical_Prop.not_or_and in Hdiff.
-  destruct Hdiff as [Hmiddle1 Hmiddle2]. rewrite middle_comm. now rewrite <- obs_fst in Hmiddle1 |- *. }
+  assert (Hdiff := @loc_g1_diff_others config ltac:(auto)).
+  apply middle_diff in Hdiff.
+  rewrite InA_cons, InA_singleton in Hdiff.
+  destruct (@bivalent_get_location_cases config ltac:(auto) id) as [Heq | Heq];
+  rewrite Heq; intuition. }
 assert (Hmoving : active da = moving gatherR2 da config).
 { unfold active, moving. induction names as [| id l]; try reflexivity; [].
   cbn -[get_location equiv_dec equiv].
@@ -3106,17 +3409,14 @@ assert (Hmoving : active da = moving gatherR2 da config).
   + exfalso. revert_one @complement.
     rewrite (round_simplify_color_bivalent id).
     changeR2. rewrite Hactive. intuition. }
-assert (Nat.div2 (nG + nB) > 0) by auto.
-destruct (active da) as [| id_move l_active] eqn:Heq_active; [cbn in *; lia |].
-destruct (idle da) as [| id_inactive l_inactive] eqn:Heq_idle; [cbn in *; lia |].
-cbn [hd] in Hloc. rewrite <- Heq_active, <- Heq_idle in *.
-pose (pt1 := get_location (config id_move)).
-pose (pt2 := find_other_loc (fst (!!! (config, (0%VS, witness)))) pt1).
 assert (Hpt1 : In pt1 (fst (!!! (config, (0%VS, witness))))). { apply pos_in_config. }
 assert (Hperm := find_other_loc_spec _ Hbivalent Hpt1). fold pt2 in Hperm.
-assert (Hmiddle_diff_2 : middle pt1 pt2 =/= pt2).
-{ assert (Hmiddle := middle_diff (find_other_loc_diff _ Hbivalent Hpt1)).
-  rewrite InA_cons, InA_singleton in Hmiddle. rewrite middle_comm. intuition. }
+assert (Hmiddle_diff_2 : middle loc_g1 loc_others =/= pt2).
+{ rewrite <- obs_fst, have_support, PermutationA_2 in Hperm; auto; [].
+  assert (Hmiddle := middle_diff (find_other_loc_diff _ Hbivalent Hpt1)). fold pt2 in Hmiddle.
+  rewrite InA_cons, InA_singleton in Hmiddle.
+  destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite Heq1, Heq2; clear -Hmiddle;
+  solve [intuition | rewrite middle_comm; intuition]. }
 (* Let us explicit the configuration *)
 assert (Hconfig : config == fun id => if activate da id then (pt1, true) else (pt2, true)).
 { intro id. specialize (Hwhite id).
@@ -3129,12 +3429,11 @@ assert (Hconfig : config == fun id => if activate da id then (pt1, true) else (p
     destruct (config id); intuition. }
 (* Then we can explicit the configuration after the round *)
 assert (Hconfig' : round gatherR2 da config
-                   == fun id => if activate da id then (middle pt1 pt2, false) else (pt2, true)).
+                   == fun id => if activate da id then (middle loc_g1 loc_others, false) else (pt2, true)).
 { intro id. rewrite (round_simplify_color_bivalent id).
   destruct_match_eq Hactive.
-  + cbn zeta. assert (Hlight := observer_light_get_light config id). changeR2.
-    rewrite Hlight, Hwhite. split; cbn [fst]; try reflexivity; [].
-    rewrite <- active_spec, Hloc, on_loc_spec in Hactive. now rewrite Hactive.
+  + cbn zeta. assert (Hlight := observer_light_get_light config id).
+    changeR2. now rewrite Hlight, Hwhite.
   + rewrite <- not_true_iff_false, <- active_spec, Hloc, on_loc_spec in Hactive. fold pt1 in Hactive.
     assert (Hin := pos_in_config config (0%VS, witness) id).
     rewrite <- support_spec, Hperm, InA_cons, InA_singleton in Hin.
@@ -3144,21 +3443,21 @@ apply dep_and; clear dep_and.
 * (* bivalent at the next round *)
   assert (Hcol := Hcolor). destruct Hcol as [Heven [Hle _]].
   repeat split; trivial; []. changeR2.
-  exists (middle pt1 pt2), pt2.
+  exists (middle loc_g1 loc_others), pt2.
   repeat split.
   + assumption.
   + destruct (obs_from_config_spec (round gatherR2 da config) (0%VS, witness)) as [Hobs _].
-    specialize (Hobs (middle pt1 pt2)).
+    specialize (Hobs (middle loc_g1 loc_others)).
     rewrite config_list_spec, map_map, <- obs_fst in Hobs. changeR2.
     rewrite Hobs, count_filter_length, filter_map, map_length.
     assert (Hfun : (eq ==> eq)%signature (activate da)
-             (fun id => if get_location (round gatherR2 da config id) =?= middle pt1 pt2
+             (fun id => if get_location (round gatherR2 da config id) =?= middle loc_g1 loc_others
                         then true else false)).
     { intros xx id ?. subst xx. destruct_match.
       + revert_one equiv. rewrite (Hconfig' id). destruct_match; intuition.
       + revert_one @complement. rewrite (Hconfig' id). destruct_match; intuition. }
     rewrite <- (filter_extensionalityA_compat Hfun (reflexivity names)).
-    apply Hlen.
+    apply Hlen_active.
   + destruct (obs_from_config_spec (round gatherR2 da config) (0%VS, witness)) as [Hobs _].
     specialize (Hobs pt2).
     rewrite config_list_spec, map_map, <- obs_fst in Hobs. changeR2.
@@ -3174,39 +3473,24 @@ apply dep_and; clear dep_and.
   intros Hbivalent' [Heven [Hn [pt1_biv [pt2_biv [Hdiff_biv [Hpt1_biv [Hpt2_biv Hcol]]]]]]].
   changeR2.
   assert (Hperm2 : PermutationA equiv (cons pt1_biv (cons pt2_biv nil))
-                                      (cons (middle pt1 pt2) (cons pt2 nil))).
-  { transitivity (support (!! (round gatherR2 da config))).
-    * apply NoDupA_inclA_length_PermutationA; autoclass.
-      + repeat constructor.
-        - now rewrite InA_singleton.
-        - now rewrite InA_nil.
-      + intros x Hin. rewrite InA_cons, InA_singleton in Hin.
-        destruct Hin as [Hin | Hin]; rewrite Hin, support_spec; unfold In; changeR2; lia.
-      + eapply bivalent_size with (st := (0%VS, witness)) in Hbivalent'.
-        now rewrite obs_fst, Hbivalent'.
-    * symmetry. apply NoDupA_inclA_length_PermutationA; autoclass.
-      + repeat constructor.
-        - now rewrite InA_singleton.
-        - now rewrite InA_nil.
-      + intros x Hin. rewrite InA_cons, InA_singleton in Hin.
-        rewrite support_spec.
-        assert (In (middle pt1 pt2) (!! (round gatherR2 da config))).
-        { rewrite obs_from_config_In. exists id_move.
-          rewrite (Hconfig' id_move).
-          assert (Heq : activate da id_move = true).
-          { rewrite <- active_spec, Heq_active. now left. }
-          now rewrite Heq. }
-        assert (In pt2 (!! (round gatherR2 da config))).
-        { rewrite obs_from_config_In. exists id_inactive.
-          rewrite (Hconfig' id_inactive).
-          assert (Heq : activate da id_inactive = false).
-          { rewrite <- idle_spec, Heq_idle. now left. }
-          now rewrite Heq. }
-        unfold In. destruct Hin as [Hin | Hin]; now rewrite Hin.
-      + eapply bivalent_size with (st := (0%VS, witness)) in Hbivalent'.
-        now rewrite obs_fst, Hbivalent'. }
+                                      (cons (middle loc_g1 loc_others) (cons pt2 nil))).
+  { transitivity (support (fst (!!! (round gatherR2 da config, (0%VS, witness))))).
+    + symmetry. changeR2. apply bivalent_support; auto.
+    + changeR2. apply bivalent_support; auto.
+      - rewrite <- obs_fst, obs_from_config_In.
+        exists id_move.
+        rewrite (Hconfig' id_move).
+        assert (Hin : List.In id_move (active da)).
+        { rewrite Heq_active. now left. }
+        rewrite active_spec in Hin. now rewrite Hin.
+      - rewrite <- obs_fst, obs_from_config_In.
+        exists id_inactive.
+        rewrite (Hconfig' id_inactive).
+        assert (Hin : List.In id_inactive (idle da)).
+        { rewrite Heq_idle. now left. }
+        rewrite idle_spec in Hin. now rewrite Hin. }
   apply PermutationA_2 in Hperm2; autoclass.
-  assert (Hsame_col : (colors (snd (!!! (round gatherR2 da config, (0%VS, witness)))))[(middle pt1 pt2, true)]
+  assert (Hsame_col : (colors (snd (!!! (round gatherR2 da config, (0%VS, witness)))))[(middle loc_g1 loc_others, true)]
                     = (colors (snd (!!! (round gatherR2 da config, (0%VS, witness)))))[(pt2, true)]).
   { rewrite Forall_forall in Hcol.
     destruct Hperm2 as [[Heq1 Heq2] | [Heq1 Heq2]].
@@ -3215,11 +3499,11 @@ apply dep_and; clear dep_and.
   (* One tower is fully black while the other is fully white, which is not color bivalent. *)
   revert Hsame_col.
   destruct (obs_from_config_spec (round gatherR2 da config) (0%VS, witness)) as [_ [_ Hobs]].
-  rewrite (Hobs (middle pt1 pt2, true)). specialize (Hobs (pt2, true)).
+  rewrite (Hobs (middle loc_g1 loc_others, true)). specialize (Hobs (pt2, true)).
   progress change bool with (@L Lght) in *. rewrite Hobs.
   rewrite config_list_spec, 2 count_filter_length, 2 filter_map, 2 map_length.
   assert (Hfun1 : (eq ==> eq)%signature (fun _ => false)
-             (fun id => if round gatherR2 da config id =?= (middle pt1 pt2, true)
+             (fun id => if round gatherR2 da config id =?= (middle loc_g1 loc_others, true)
                         then true else false)).
   { intros xx id ?. subst xx. destruct_match; trivial; [].
     revert_one equiv. rewrite (Hconfig' id). destruct_match.
@@ -3236,7 +3520,7 @@ apply dep_and; clear dep_and.
   rewrite <- (filter_extensionalityA_compat Hfun2 (reflexivity names)).
   assert (Heq0 : length (List.filter (fun _ : ident => false) names) = 0).
   { induction names; auto. }
-  unfold idle in *. rewrite Heq0, Hidle. lia.
+  unfold idle in *. rewrite Heq0, Hlen_idle. lia.
 Qed.
 
 Definition cb_b_precondition_only_black_active :=
@@ -3272,36 +3556,31 @@ Lemma color_bivalent_next_bivalent_only_black_active :
 Proof using Hssync Hcolor.
 intros [Hallblack Htowers].
 assert (Hconfig' := a3b_next_round Hallblack).
-assert (Hsame_loc := a3b_same_loc Hallblack).
+assert (Hsame_loc := a3b_same_loc).
 assert (Hsame_obs := a3b_same_obs Hallblack).
-assert (Hcol := Hcolor). destruct Hcol as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 Hcol]]]]]]].
 assert (dep_and : forall A B : Prop, A -> (A -> B) -> A /\ B) by intuition.
 apply dep_and; clear dep_and.
 * (* bivalent after the round *)
-  repeat split; trivial; []. changeR2.
-  exists pt1, pt2. repeat split; trivial; [|]; now rewrite Hsame_obs.
+  repeat split; eauto; []. changeR2.
+  exists loc_g1, loc_others. rewrite Hsame_obs. auto.
 * (* not color bivalent after the round *)
   intros Hbivalent' [_ [_ [pt1_biv [pt2_biv [Hdiff_biv [Hpt1_biv [Hpt2_biv Hcol']]]]]]].
-  assert (Hperm1 := have_support).
-  rewrite <- Hsame_obs, (obs_fst (0%VS, witness)) in Hperm1. changeR2.
+  assert (Hperm1 := @have_support config ltac:(auto)).
+  rewrite <- Hsame_obs, obs_fst in Hperm1. changeR2.
   revert Hperm1 Hcol'.
   set (obs := (!!! (round gatherR2 da config, (0%VS, witness)))).
   intros Hperm1 Hcol'.
   assert (Hperm2 : PermutationA equiv (support (fst obs)) (cons pt1_biv (cons pt2_biv nil))).
   { apply (bivalent_support Hbivalent'); auto. }
-  assert (Hperm3 : PermutationA equiv (support (fst obs)) (cons pt1 (cons pt2 nil))).
-  { apply (bivalent_support Hbivalent'); auto; apply mult_div2_In; try lia; now rewrite Hsame_obs. }
-  assert (Hblack' : (colors (snd (!!! (round gatherR2 da config, (0%VS, witness)))))[(pt1, false)]
-                  = (colors (snd (!!! (round gatherR2 da config, (0%VS, witness)))))[(pt2, false)]).
-  { rewrite Hperm2 in Hperm3.
-    apply PermutationA_2 in Hperm3; autoclass; [].
+  assert (Hblack' : (colors (snd (!!! (round gatherR2 da config, (0%VS, witness)))))[(loc_g1, false)]
+                  = (colors (snd (!!! (round gatherR2 da config, (0%VS, witness)))))[(loc_others, false)]).
+  { rewrite Hperm1 in Hperm2.
+    apply PermutationA_2 in Hperm2; autoclass; [].
     rewrite Forall_forall in Hcol'. changeR2.
-    destruct Hperm3 as [[Heq1 Heq2] | [Heq1 Heq2]];
-    rewrite <- Heq1, <- Heq2; rewrite Hcol'; reflexivity || now right; left. }
+    destruct Hperm2 as [[Heq1 Heq2] | [Heq1 Heq2]];
+    rewrite Heq1, Heq2; rewrite Hcol'; reflexivity || now right; left. }
   clear Hcol' Hpt1_biv Hpt2_biv. revert Hblack'.
-  changeR2. rewrite Forall_forall in Hcol.
-  assert (Hblack : List.In false l_list) by now right; left.
-  apply Hcol in Hblack. clear Hcol.
+  changeR2. assert (Hcol := same_colors).
   (* Let us express the number of black robots on each tower after one round. *)
   destruct (obs_from_config_spec (round gatherR2 da config) (0%VS, witness)) as [_ [_ Hobs']].
   do 2 rewrite Hobs', config_list_spec, count_filter_length, filter_map, map_length.
@@ -3311,25 +3590,20 @@ apply dep_and; clear dep_and.
              (fun id => (config id ==b (pt, false)) && negb (activate da id))).
   { intros pt xx id ?. subst xx.
     rewrite 2 state_eqb, a3b_same_loc, a3b_next_black_eqb; intuition. }
-  rewrite (filter_extensionalityA_compat (Hfun pt1) (reflexivity names)),
-          (filter_extensionalityA_compat (Hfun pt2) (reflexivity names)).
+  rewrite (filter_extensionalityA_compat (Hfun loc_g1) (reflexivity names)),
+          (filter_extensionalityA_compat (Hfun loc_others) (reflexivity names)).
   (* Then, let us split robots wrt colors, location, activation and simplify. *)
-  rewrite (active_idle_is_partition da), idle_split, 2 idle_on_split.
+  rewrite (active_idle_is_partition da), (@idle_split config), 2 idle_on_split; auto.
   repeat rewrite ?filter_app, ?app_length.
-  rewrite 2 a3b_length_idle_active, 4 a3b_length_white_idle, 4 a3b_length_black_idle.
+  rewrite 2 a3b_length_idle_active, 4 a3b_length_white_idle, 4 a3b_length_black_idle_eq.
+  assert (loc_g1 =/= loc_others) by auto.
   cut (length black_idle_on_g1 <> length black_idle_on_other).
-  { rewrite Hperm1 in Hperm3. apply PermutationA_2 in Hperm3; auto; [].
-    Time destruct Hperm3 as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite Heq1, Heq2; simpl_bool;
-    do 2 destruct_match; reflect_bool; try (now elim Hdiff); rewrite <- Heq1, <- Heq2; lia. }
-  assert (Hblack' : length black_on_g1 = length black_on_other).
-  { rewrite <- 2 length_light_on in Hblack.
-    rewrite Hperm1 in Hperm3. apply PermutationA_2 in Hperm3; auto; [].
-    now destruct Hperm3 as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite Heq1, Heq2. }
-  clear Hblack.
+  { simpl_bool; do 2 destruct_match; reflect_bool; auto. lia. }
+  assert (Hblack' := color_bivalent_length_black).
   assert (Hlen : forall pt, length (black_idle_on pt config) + length (active_on pt config)
                             = length (black_on pt config)).
   { intro pt. rewrite <- a3b_black_active_is_active; trivial; [].
-    unfold black_idle_on, black_on, active_on, idle_on.
+    unfold black_idle_on, black_active_on, black_on, active_on, idle_on.
     now rewrite Nat.add_comm, <- app_length, <- 2 filter_app, <- active_idle_is_partition. }
   assert (Hpt1' := Hlen loc_g1). specialize (Hlen loc_others).
   lia.
@@ -3366,7 +3640,7 @@ cut (Nat.div2 (nG + nB) < (!! (round gatherR2 da config))[get_location (round ga
 assert (Hmult : (!! config)[get_location (config id1)] = Nat.div2 (nG + nB)).
 { assert (Hperm : PermutationA equiv (cons (get_location (config id1)) (cons (get_location (config id2)) nil))
                                     (cons loc_g1 (cons loc_others nil))).
-  { etransitivity; [| apply have_support]. symmetry. rewrite obs_fst.
+  { etransitivity; [| apply have_support; auto]. symmetry. rewrite obs_fst.
     apply (bivalent_support (config := config)); auto. }
   rewrite PermutationA_2 in Hperm; auto; [].
   destruct Hperm as [[Heq _] | [Heq _ ]]; rewrite Heq; auto. }
@@ -3400,16 +3674,14 @@ assert (Hmiddle : middle loc_g1 loc_others
 { assert (Hperm : PermutationA equiv (support (fst (!!! (config, (0%VS, witness)))))
                   (cons (get_location (config id1)) (cons (get_location (config id2)) nil))).
   { apply (bivalent_support (color_bivalent_bivalent Hcolor) (0%VS, witness)); auto. }
-  rewrite have_support in Hperm.
+  rewrite <- obs_fst, have_support in Hperm; auto.
   apply PermutationA_2 in Hperm; auto; [].
-  destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite Heq1, Heq2.
-  - reflexivity.
-  - now rewrite middle_comm. }
+  destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite Heq1, Heq2; auto; apply middle_comm. }
 assert (Hsupp : PermutationA equiv (support (!! (round gatherR2 da config)))
                   (cons (get_location (config id1)) (cons (get_location (config id2)) nil))).
 { rewrite obs_fst. apply (bivalent_support Hbivalent (0%VS, witness)); auto.
-  - rewrite <- Hid1. apply pos_in_config.
-  - rewrite <- Hid2. apply pos_in_config. }
+  - rewrite <- Hid1. auto.
+  - rewrite <- Hid2. auto. }
 assert (Hin := pos_in_config (round gatherR2 da config) (0%VS, witness) id_move).
 rewrite Hid_move, Hmiddle, <- support_spec, Hsupp in Hin.
 apply middle_diff in Hdiff.
@@ -3699,7 +3971,8 @@ destruct (active da) as [| id l] eqn:Hactive.
     { eapply (@PermutationA_nil _ equiv _);try typeclasses eauto.
       rewrite <- Hactive.
       symmetry.
-      apply active_split. }
+      apply active_split.
+      auto. }
     apply app_eq_nil in H.
     destruct H as [heq1 heq2].
     now rewrite heq1,heq2.
@@ -3964,12 +4237,8 @@ destruct (active da) as [| id l] eqn:Hactive.
           assumption.
         - exfalso.
           specialize (h_forall id_move).
-          apply h_forall;auto. }
+          apply h_forall; auto. }
 
-      (* destruct (exists_dec id', id' colocated with id_move /\ ~ is_moving id)
-         - trivial.
-         - by (h_cb_nb_wm id_move) the case where all robots on id_move move implies that there are
-           exactly (div2 n) robots moving, which is contradictory. *)
       assert ((exists id'', get_location (config id'') = get_location (config id_move)
                             /\ ~ is_moving gatherR2 da config id'')
               \/ ~(exists id'', get_location (config id'') = get_location (config id_move)
@@ -4014,7 +4283,9 @@ destruct (active da) as [| id l] eqn:Hactive.
           exfalso.
           specialize (color_bivalent_bivalent Hcolor) as hcolor.
 
-          assert (hbiv := fun pt3 id3 => @bivalent_same_location_2 _ _ _ _ _ (get_location (config id_move)) (get_location (config id')) pt3 id_move id' id3 hcolor eq_refl eq_refl).
+          assert (hbiv := fun pt3 id3 => @bivalent_same_location_2 _ _ _ _ _
+                                           (get_location (config id_move)) (get_location (config id'))
+                                           pt3 id_move id' id3 hcolor eq_refl eq_refl).
           assert (forall (pt3 : location) (id3 : ident),
                      get_location (config id3) = pt3 ->
                      get_location (config id3) = get_location (config id')
@@ -4170,7 +4441,9 @@ destruct (active da) as [| id l] eqn:Hactive.
           exfalso.
           specialize (color_bivalent_bivalent Hcolor) as hcolor.
 
-          assert (hbiv := fun pt3 id3 => @bivalent_same_location_2 _ _ _ _ _ (get_location (config id_move)) (get_location (config id')) pt3 id_move id' id3 hcolor eq_refl eq_refl).
+          assert (hbiv := fun pt3 id3 => @bivalent_same_location_2 _ _ _ _ _
+                                           (get_location (config id_move)) (get_location (config id'))
+                                           pt3 id_move id' id3 hcolor eq_refl eq_refl).
           assert (forall (pt3 : location) (id3 : ident),
                      get_location (config id3) = pt3 ->
                      get_location (config id3) = get_location (config id')
@@ -4298,8 +4571,6 @@ destruct (active da) as [| id l] eqn:Hactive.
   }
 Qed.
 
-
-
 Lemma get_light_decb_spec id col: get_light (config id) = col <-> get_light_decb config col id = true.
 Proof using .
   unfold get_light_decb.
@@ -4308,19 +4579,21 @@ Proof using .
   - split;intro; try contradiction; try discriminate.
 Qed.
 
-Theorem color_bivalent_round_lt_config :
+End ColorBivalent.
+
+Theorem color_bivalent_round_lt_config : forall config, color_bivalent config ->
   changing gatherR2 da config <> nil ->
   lt_config (round gatherR2 da config) config.
-Proof.
-intro Hchanging. unfold lt_config, measure.
+Proof using Hssync.
+intros config Hcolor Hchanging. unfold lt_config, measure.
 assert (Hbivalent := color_bivalent_bivalent Hcolor).
 rewrite <- bivalent_obs_spec in Hbivalent.
 assert (Hcol := Hcolor). rewrite <- color_bivalent_obs_spec in Hcol.
 rewrite Hbivalent, Hcol.
-destruct color_bivalent_exhaustive_cases
+destruct (color_bivalent_exhaustive_cases Hcolor)
   as [Hcb | [Hb | Hnb]].
 * (* color bivalent after the round *)
-  assert (Hnext := color_bivalent_next_color_bivalent Hcb).
+  assert (Hnext := color_bivalent_next_color_bivalent Hcolor Hcb).
   assert (Hbivalent' := color_bivalent_bivalent Hnext).
   rewrite <- bivalent_obs_spec in Hbivalent'. rewrite <- color_bivalent_obs_spec in Hnext.
   rewrite Hbivalent', Hnext. right.
@@ -4398,14 +4671,13 @@ destruct color_bivalent_exhaustive_cases
     rewrite in_map_iff in abs.
     destruct abs as [id_abs [h_abs_black h_abs_active]].
     rewrite List.filter_In in h_abs_active.
-    destruct h_abs_active as [ _ h_active abs].
+    destruct h_abs_active as [ _ h_active].
     assert (is_black (round gatherR2 da config) id_abs) as h''.
     { assumption. }
-    rewrite a3b_next_black in h''.
-    - destruct h'' as [h'' h'''].
-      rewrite h_active in h'''.
-      discriminate.
-    - assumption. }
+    rewrite a3b_next_black in h''; auto; [].
+    destruct h'' as [h'' h'''].
+    rewrite h_active in h'''.
+    discriminate. }
   changeR2.
   rewrite heq_0.
   destruct (changing gatherR2 da config) eqn:heq.
@@ -4429,7 +4701,6 @@ destruct color_bivalent_exhaustive_cases
       assumption. }
     rewrite h_i_black in h_i_active.
     assumption.
-      
 * (* bivalent but not color bivalent after the round *)
   assert (Hnext : bivalent (round gatherR2 da config) /\ ~ color_bivalent (round gatherR2 da config)).
   { destruct Hb as [Hb_white | Hb_black].
@@ -4451,8 +4722,6 @@ destruct color_bivalent_exhaustive_cases
   unfold old_measure. repeat destruct_match; left; lia.
 Qed.
 
-End ColorBivalent.
-
 
 Section BivalentButNotColorBivalent.
 
@@ -4466,8 +4735,7 @@ Theorem round_simplify_bivalent :
      if da.(activate) id
      then
        let obs := !!!(config, config id) in
-       let other_loc := find_other_loc (fst obs) (get_location (config id)) in
-       let maj_black := find_max_black obs (get_location (config id)) other_loc in
+       let maj_black := find_max_black obs (loc_g1 config) (loc_others config) in
        (maj_black, observer_lght (snd obs))
      else config id.
 Proof using Hssync Hbivalent Hcolor.
@@ -4486,8 +4754,7 @@ Qed.
 (* Any active robot targets the blackest tower *)
 Lemma not_color_bivalent_target : forall id, List.In id (active da) ->
   get_location (round gatherR2 da config id)
-  == find_max_black (!!! (config, config id)) (get_location (config id))
-                    (find_other_loc (fst (!!! (config, config id))) (get_location (config id))).
+  == find_max_black (!!! (config, config id)) (loc_g1 config) (loc_others config).
 Proof using Hssync Hbivalent Hcolor.
 intros id Hid.
 rewrite (round_simplify_bivalent id).
@@ -4499,81 +4766,26 @@ Corollary not_color_bivalent_moving_target : forall id, List.In id (moving gathe
   == find_other_loc (fst (!!! (config, config id))) (get_location (config id)).
 Proof using Hssync Hbivalent Hcolor.
 intros id Hid.
-rewrite not_color_bivalent_target.
-+ rewrite moving_spec in Hid.
-  match goal with |- find_max_black ?a ?b ?c == _ =>
-    destruct (find_max_black_either a b c)
-  end; auto; [].
-  rewrite <- not_color_bivalent_target in * |-; auto; [].
-  rewrite <- moving_spec in Hid. revert Hid. now apply moving_active.
-+ revert Hid. now apply moving_active.
-Qed.
-
-(* TODO: see if it is useful elsewhere *)
-Lemma wlog_sym : forall (x y : location) P, Proper (equiv ==> equiv ==> iff) P ->
-  (P x y -> P y x) ->
-  forall x' y', PermutationA equiv (cons x (cons y nil)) (cons x' (cons y' nil)) ->
-  P x y -> P x' y'.
-Proof.
-intros x y P HP Hsym x' y' Hperm HPxy.
-rewrite PermutationA_2 in Hperm; auto; [].
- destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite <- Heq1, <- Heq2; auto.
-Qed.
-
-Lemma find_max_black_comm :
-  forall st pt1 pt2,
-    In pt1 (!! config) -> In pt2 (!! config) ->
-    find_max_black (!!! (config, st)) pt1 pt2 == find_max_black (!!! (config, st)) pt2 pt1.
-Proof.
-intros st pt1 pt2 Hin1 Hin2. unfold find_max_black.
-repeat destruct_match; try reflexivity || (rewrite Nat.leb_gt in *; lia); [].
-destruct (pt1 =?= pt2) as [? | Hneq]; auto; [].
-exfalso. apply Hcolor.
-assert (Hbiv := Hbivalent). destruct Hbiv as [Heven [Hn [pt1' [pt2' [Hdiff [Hpt1' Hpt2']]]]]].
-repeat split; trivial; [].
-exists pt1', pt2'. repeat split; trivial; [].
-assert (Heq : (colors (snd (!!! (config, st))))[(pt1, false)]
-            = (colors (snd (!!! (config, st))))[(pt2, false)]).
-{ rewrite Nat.leb_le in *. lia. }
-pattern pt1', pt2'.
-apply (@wlog_sym pt1 pt2).
-* intros ? ? Heq1 ? ? Heq2. rewrite 2 Forall_forall. now rewrite Heq1, Heq2.
-* rewrite 2 Forall_forall. intros Hsym l Hl. symmetry; auto.
-* transitivity (support (!! config)); rewrite (obs_fst (0%VS, witness)); changeR2.
-  + symmetry. apply bivalent_support; auto.
-  + apply bivalent_support; auto; rewrite <- obs_fst; now apply mult_div2_In.
-* rewrite Forall_forall. intros [] _; trivial; [].
-  (* white *)
-  rewrite <- 2 length_light_on in *.
-  rewrite 2 (colors_indep config (0%VS, witness) (0%VS, witness)), <- 2 length_light_on in Heq.
-  rewrite bivalent_In_iff_mult_eq_half in Hin1, Hin2; auto.
-  assert (Hlen : length (on_loc pt1 config) = length (on_loc pt2 config)).
-  { now rewrite <- (obs_from_config_on_loc _ (0%VS, witness)), Hin1, <- Hin2, obs_from_config_on_loc. }
-  rewrite (on_loc_color_split pt1 config), (on_loc_color_split pt2 config), 2 app_length in Hlen.
-  lia.
+assert (List.In id (active da)).
+{ revert Hid. now apply moving_active. }
+rewrite not_color_bivalent_target; auto.
+rewrite moving_spec in Hid.
+changeR2.
+match goal with |- find_max_black ?a ?b ?c == _ =>
+  destruct (find_max_black_either a b c) as [Heq1 | Heq1]
+end;
+destruct (bivalent_get_location_cases Hbivalent id) as [Heq2 | Heq2];
+rewrite <- not_color_bivalent_target in * |- *; rewrite ?Heq1, ?Heq2; auto.
+- congruence.
+- now rewrite fold_obs_fst, find_other_loc_loc_others.
+- congruence.
 Qed.
 
 Lemma not_color_bivalent_same_destination : same_destination_if_active gatherR2 da config.
 Proof using Hssync Hbivalent Hcolor.
 intros id1 id2 Hid1 Hid2.
-assert (Hbiv := Hbivalent).
-destruct Hbiv as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 Hpt2]]]]]]. changeR2.
 etransitivity; [now eapply not_color_bivalent_target; eauto |].
-rewrite not_color_bivalent_target; trivial; [].
-assert (Hcase : get_location (config id1) == get_location (config id2)
-        \/ (get_location (config id1) == find_other_loc (fst (!!! (config, config id2))) (get_location (config id2))
-         /\ get_location (config id2) == find_other_loc (fst (!!! (config, config id1))) (get_location (config id1)))).
-{ destruct (get_location (config id1) =?= get_location (config id2)).
-  + now left.
-  + right.
-    assert (Hobs1 : In (get_location (config id1)) (fst (!!! (config, config id1)))) by apply pos_in_config.
-    apply find_other_loc_spec in Hobs1; try (now rewrite bivalent_obs_spec); [].
-    assert (Hobs2 : In (get_location (config id2)) (fst (!!! (config, config id2)))) by apply pos_in_config.
-    apply find_other_loc_spec in Hobs2; try (now rewrite bivalent_obs_spec); [].
-    rewrite Hobs1, PermutationA_2 in Hobs2; auto; []. intuition. }
-destruct Hcase as [Heq1 | [Heq1 Heq2]]; rewrite <- Heq1, <- ?Heq2.
-+ reflexivity.
-+ rewrite find_max_black_comm; auto; apply pos_in_config.
+now rewrite not_color_bivalent_target.
 Qed.
 
 Theorem not_color_bivalent_wither_and_grow : forall id,
@@ -4616,22 +4828,15 @@ induction names as [| id' l]; cbn [List.map].
       destruct Htest as [? Htest]. changeR2. setoid_rewrite Htest. clear Htest.
       destruct_match; now idtac + apply le_S; apply IHl.
     - (* As id moves, the target is its ending location. *)
-      assert (Htest : exists H, find_max_black (!!! (config, config id')) (get_location (config id'))
-                        (find_other_loc (fst (!!! (config, config id'))) (get_location (config id'))) =?= pt' = left H).
+      assert (Htest : exists H, find_max_black (!!! (config, config id')) (loc_g1 config) (loc_others config)
+                                =?= pt' = left H).
       { clear IHl.
-        destruct (find_max_black (!!! (config, config id')) (get_location (config id'))
-                     (find_other_loc (fst (!!! (config, config id'))) (get_location (config id')))
+        destruct (find_max_black (!!! (config, config id')) (loc_g1 config) (loc_others config)
                   =?= pt') as [? | Hneq]; eauto; [].
-        assert (Hdiff := Hmove). rewrite moving_spec in Hdiff. rewrite <- active_spec in Hactive.
-        assert (Hbiv := Hbivalent). rewrite <- bivalent_obs_spec with (st := config id') in Hbiv.
-        assert (Hperm := find_other_loc_spec _ Hbiv (pos_in_config _ _ id')). changeR2.
         exfalso. apply Hneq. clear Hneq.
-        rewrite <- not_color_bivalent_target, <- Heq'; trivial; [].
-        rewrite not_color_bivalent_target in Hdiff |- *;
-        try (now apply (moving_active Hssync gatherR2 config id)); [].
-        match goal with |- find_max_black ?a ?b ?c == _ =>
-          destruct (find_max_black_either a b c)
-        end; auto. }
+        rewrite <- active_spec in Hactive.
+        rewrite <- not_color_bivalent_target, <- Heq',
+                not_color_bivalent_moving_target, fold_obs_fst; auto. }
       destruct Htest as [? Htest]. changeR2. rewrite Htest. clear Htest.
       repeat destruct_match; now apply le_n_S + apply le_S; apply IHl.
   + cbn [countA_occ]. split; intros; destruct_match; try apply le_n_S; apply IHl; auto.
@@ -4649,7 +4854,7 @@ set (pt_id := get_location (config id)).
 set (pt'_id := find_other_loc (!! config) pt_id).
 Unshelve.
 assert (pt'_id =/= pt_id).
-{ unfold pt'_id. rewrite (obs_fst (config id)). apply find_other_loc_diff.
+{ unfold pt'_id. rewrite obs_fst. apply find_other_loc_diff.
   - now rewrite bivalent_obs_spec.
   - apply pos_in_config. }
 assert (In pt'_id (fst (!!! (config, config id)))).
@@ -4662,10 +4867,10 @@ assert (Hsame : (!! config)[pt_id] = (!! config)[pt'_id]).
 { inversion Hbivalent as [Heven Hbiv]. destruct Hbiv as [Hle [pt1 [pt2 [Hdiff [Hpt1 Hpt2]]]]].
   assert (Hcase : pt1 == pt_id /\ pt2 == pt'_id \/ pt1 == pt'_id /\ pt2 == pt_id).
   { assert (In pt1 (fst (!!! (config, config id)))).
-    { unfold In. rewrite <- obs_fst. changeR2. rewrite Hpt1.
+    { unfold In. rewrite fold_obs_fst. changeR2. rewrite Hpt1.
       apply Exp_prop.div2_not_R0. lia. }
     assert (In pt2 (fst (!!! (config, config id)))).
-    { unfold In. rewrite <- obs_fst. changeR2. rewrite Hpt2.
+    { unfold In. rewrite fold_obs_fst. changeR2. rewrite Hpt2.
       apply Exp_prop.div2_not_R0. lia. }
     changeR2. destruct (pt1 =?= pt_id) as [Heq | Heq].
     * left. split; trivial; [].
@@ -5969,7 +6174,7 @@ destruct (support (max (!! (round gatherR2 da config)))) as [| pt1 [| pt2 l]] eq
               ++ { exfalso.
                    assert(hpermut_config: PermutationA equiv (support (!! (round gatherR2 da config)))
                                                            (pt2 :: pt1 :: nil)).
-                   { assert (hpermut12:PermutationA equiv (pt1 :: pt2 :: nil) (pt2 :: pt1 :: nil))  by permut_3_4.
+                   { assert (hpermut12:PermutationA equiv (pt1 :: pt2 :: nil) (pt2 :: pt1 :: nil)) by permut_3_4.
                      rewrite hpermut12 in h_incl_pt1_pt2.
                      rewrite heq_pt2_bary in heq2, h_incl_pt1_pt2.
                      apply inclA_cons_inv in h_incl_pt1_pt2;autoclass.
@@ -6729,7 +6934,7 @@ destruct (bivalent_dec config) as [Hbivalent | Hbivalent].
     rewrite MajTower_at_equiv in Hmaj.
     assert (Hsupp : PermutationA equiv (support (max (!! (round gatherR2 da config)))) (cons pt nil)).
     { now rewrite Hmaj. }
-    rewrite (obs_fst (origin, witness)) in Hsupp.
+    rewrite obs_fst in Hsupp.
     changeR2. apply PermutationA_length1 in Hsupp; autoclass; [].
     destruct Hsupp as [pt' [Hpt' Hsupp]]. rewrite Hsupp.
     left. lia.
@@ -6817,46 +7022,25 @@ destruct (bivalent_dec config) as [Hbivalent | Hbivalent].
     - unfold obs in *. setoid_rewrite observer_light_get_light in Hlight.
       intro Habs. rewrite <- Habs in *. discriminate.
   + (* Bivalent case: Robots not on the blackest tower try to reach it *)
-    destruct (proj1 (extend_bivalent config) Hbivalent)
-      as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 [Hsupp [Hin Hother]]]]]]]]].
-    changeR2.
-    assert (Nat.div2 (nG + nB) > 0). { apply Exp_prop.div2_not_R0. lia. }
-    destruct (find_max_black_either (!!! (config, (origin, witness))) pt1 pt2) as [Hmax | Hmax].
-    - assert (Hin2 : In pt2 (!! config)). { unfold In. changeR2. now rewrite Hpt2. }
+    destruct (find_max_black_either (!!! (config, (origin, witness))) (loc_g1 config) (loc_others config))
+      as [Hmax | Hmax].
+    - (* g1 is on the blackest tower, so we use the other one *)
+      assert (Hin2 : In (loc_others config) (!! config)). { now apply loc_others_In. }
       rewrite obs_from_config_In in Hin2. destruct Hin2 as [gmove Hgmove].
       exists gmove. intros da Hssync Hactive.
-      assert (Htarget : get_location (round gatherR2 da config gmove) == pt1).
-      { rewrite not_color_bivalent_target, <- Hmax; trivial; [].
-        rewrite find_max_black_indep, find_max_black_comm; auto; [| |].
-        - f_equiv; trivial; [].
-          assert (Hperm : In pt2 (!! config)).
-          { changeR2. rewrite <- support_spec, Hsupp. now right; left. }
-          rewrite (obs_fst (config id)) in Hperm.
-          apply find_other_loc_spec in Hperm; try (now rewrite bivalent_obs_spec); [].
-          rewrite <- obs_fst in Hperm. changeR2. rewrite Hsupp in Hperm.
-          rewrite PermutationA_2 in Hperm; autoclass; [].
-          rewrite <- obs_fst, Hgmove. changeR2. intuition.
-        - apply pos_in_config.
-        - apply find_other_loc_In, pos_in_config; []. now rewrite bivalent_obs_spec. }
+      assert (Htarget : get_location (round gatherR2 da config gmove) == loc_g1 config).
+      { now rewrite not_color_bivalent_target. }
       apply moving_changing; auto; [].
-      now rewrite moving_spec, Htarget, Hgmove.
-    - (* Symmetrical case *)
-      assert (Hin1 : In pt1 (!! config)). { unfold In. changeR2. now rewrite Hpt1. }
-      rewrite obs_from_config_In in Hin1. destruct Hin1 as [gmove Hgmove].
+      rewrite moving_spec, Htarget, Hgmove.
+      now apply loc_g1_diff_others. (* auto should work here *)
+    - (* Symmetrical case: g1 is not on the blackest tower, so we can use it *)
+      pose (gmove := Good g1).
       exists gmove. intros da Hssync Hactive.
-      assert (Htarget : get_location (round gatherR2 da config gmove) == pt2).
-      { rewrite not_color_bivalent_target, <- Hmax; trivial; [].
-        rewrite find_max_black_indep; trivial; [].
-        f_equiv; trivial; [].
-        assert (Hperm : In pt1 (!! config)).
-        { changeR2. rewrite <- support_spec, Hsupp. now left. }
-        rewrite (obs_fst (config id)) in Hperm.
-        apply find_other_loc_spec in Hperm; try (now rewrite bivalent_obs_spec); [].
-        rewrite <- obs_fst in Hperm. changeR2. rewrite Hsupp in Hperm.
-        rewrite PermutationA_2 in Hperm; autoclass; [].
-        rewrite <- obs_fst, Hgmove. changeR2. intuition. }
+      assert (Htarget : get_location (round gatherR2 da config gmove) == loc_others config).
+      { now rewrite not_color_bivalent_target. }
       apply moving_changing; auto; [].
-      now rewrite moving_spec, Htarget, Hgmove.
+      rewrite moving_spec, Htarget.
+      now apply loc_others_diff_g1.
 * destruct (support (max (!! config))) as [| pt [| pt' lmax]] eqn:Hmax.
   + elim (support_max_non_nil _ Hmax).
   + rewrite <- MajTower_at_equiv in Hmax.
diff --git a/CaseStudies/Gathering/WithMultiplicityLight.v b/CaseStudies/Gathering/WithMultiplicityLight.v
index 25d6a7a890f6f395fe750cfffbd890521a500f76..9c31669affcdfbf1ff0eebcf32249b5f6ed60491 100644
--- a/CaseStudies/Gathering/WithMultiplicityLight.v
+++ b/CaseStudies/Gathering/WithMultiplicityLight.v
@@ -1261,7 +1261,10 @@ destruct (Nat.eq_0_gt_0_cases (!!config)[pt]) as [| Hlt]; trivial; [].
 elim Hdiff. apply (bivalent_same_location _ _ pt Hbivalent Hpt1 Hpt2); intuition.
 Qed.
 
-Lemma obs_fst : forall st config, !! config == fst (!!!(config, st)).
+Lemma obs_fst : forall config, !! config == fst (!!!(config, (origin, witness))).
+Proof. reflexivity. Qed.
+
+Lemma fold_obs_fst : forall st config, fst (!!!(config, st)) == !! config.
 Proof. reflexivity. Qed.
 
 Definition bivalent_extended (config : configuration) :=
@@ -1424,15 +1427,16 @@ Proof using .
   apply andb_prop in h_and.
   destruct h_and as [ heq_loc h_forall].
   apply Nat.eqb_eq in heq_loc.
+  rewrite <- (obs_from_config_fst_ok (origin, witness)) in heq_loc.
   rewrite  forallb_forall in h_forall.
   setoid_rewrite Nat.eqb_eq in h_forall.
-  
+
   specialize (obs_from_config_fst_spec config (origin,witness)) as h.
   specialize (h l) as h_l.
   specialize (h l1) as h_l1.
   clear h.
-  specialize (cardinal_fst_obs_from_config config (origin,witness)) as h_cardinal.
-  rewrite <- obs_fst in *.
+  assert (h_cardinal := cardinal_fst_obs_from_config config (origin,witness)).
+  rewrite <- obs_fst in h_cardinal.
   rewrite cardinal_fold_support in h_cardinal.
   rewrite <- obs_from_config_fst_ok with (st:=(0%VS, witness)) in H.
   rewrite H in h_cardinal.