diff --git a/CaseStudies/Gathering/InR2/Algorithm.v b/CaseStudies/Gathering/InR2/Algorithm.v
index 0e41326fdff4483b27953ac0f8cfbd5f8f1c704d..37ac2f308f8e41dd8b1e9f24c8a56a82912a56c8 100644
--- a/CaseStudies/Gathering/InR2/Algorithm.v
+++ b/CaseStudies/Gathering/InR2/Algorithm.v
@@ -2333,7 +2333,6 @@ destruct (support (max (!! (round gatherR2 da config)))) as [| pt1 [| pt2 l]] eq
            apply support_NoDupA. }
          inv_nodup hnodupxyz.
          inv_nodup hnodup.
-         (* simpl in H;lia. *)
          destruct (equiv_dec pt1 (isobarycenter_3_pts ptx pty ptz)) as [heq_pt1_bary | hneq_pt1_bary].
          ++ { exfalso.
               assert(hpermut_config: PermutationA equiv (support (!! (round gatherR2 da config)))
@@ -2624,9 +2623,8 @@ destruct (support (max (!! (round gatherR2 da config)))) as [| pt1 [| pt2 l]] eq
                   - rewrite <- Hsec'. unfold on_SEC. intro. rewrite (filter_InA _). intuition.
                   - rewrite <- size_spec. rewrite Hlen. cbn. lia. }
                 rewrite <- Hsec' in Hperm'.
-                (* Triangle equilatéral: comme qqchose bouge et que on est encore avec 3
-                   colonne après, une colonne s'est déplacée vers le barycentre, contradiction:
-                   le barycentre ne peut pas être sur le SEC. *)
+                (* Equilateral triangle: since one robot moves and there are still 3 columns afterwards,
+                   a column moved to the barycenter, contradiction as the barycenter cannot be on the SEC. *)
                 assert (Hnodup : NoDupA equiv (ptx :: pty :: ptz :: nil)).
                 { rewrite <- Hsec. apply on_SEC_NoDupA, support_NoDupA. }
                 assert (Hex : exists pta ptb ptc,
diff --git a/CaseStudies/Gathering/InR2/Algorithm_withLight.v b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
index c30a5ea8776724cd4816d18876676760afb400df..8ca2917f68be4a513f68c35c7ed1182be26ec487 100644
--- a/CaseStudies/Gathering/InR2/Algorithm_withLight.v
+++ b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
@@ -121,29 +121,29 @@ Instance NoByz : NoByzantine.
 Proof using . now split. Qed.
 
 Lemma nG_ge: nG >= 3.
-Proof.
+Proof using size_G.
   cbn.
   lia.
 Qed.
 
 Lemma nG_nonzero: nG <> 0.
-Proof.
+Proof using size_G.
   cbn.
   lia.
 Qed.
 
 Lemma le_2_n : 2 <= nG + nB.
-Proof. cbn. lia. Qed.
+Proof using size_G. cbn. lia. Qed.
 Hint Resolve le_2_n : core.
 
 Lemma n_gt_0 : Nat.div2 (nG + nB) > 0.
-Proof. apply Exp_prop.div2_not_R0. cbn. lia. Qed.
+Proof using size_G. apply Exp_prop.div2_not_R0. cbn. lia. Qed.
 
 Hint Immediate n_gt_0 le_2_n : core.
 
 (** Define one robot to get the location whenever they are gathered. *)
 Definition g1 : G.
-Proof. exists 0. generalize size_G; intro; abstract lia. Defined.
+Proof using size_G. exists 0. generalize size_G; intro; abstract lia. Defined.
 
 Instance Lght: @WithMultiplicityLight.Lights.
 refine {|
@@ -191,26 +191,10 @@ Proof using . split. reflexivity. Qed.
 
 (* Trying to avoid notation problem with implicit arguments *)
 Local Notation "s [ x ]" := (multiplicity x s) (at level 2, no associativity, format "s [ x ]"): pactole_scope.
-(* Notation "!! config" := (@obs_from_config location _ _ _ multiset_observation config origin) (at level 10). *)
-
-(* false here is arbitrary here since multiset_observation_info.obs_from_config ignores it *)
-(* Notation "!! config" := *)
-  (* (@obs_from_config _ _ _ _ (@multiset_observation_info _ _ _ _ _ _ _ Permutation_refl' _) *)
-            (* config (origin,false) ) (at level 10). *)
 
 Existing Instance WithMultiplicityLight.Obs.
 
-(* Instance ObsWithLight : Observation := @WithMultiplicityLight.Obs _ bool _ _ _ MyRobots. *)
-
 Notation support := (@support location _ _ _).
-(* (@obs_from_config R2 unit _ _ _ _ _ _ multiset_observation) (at level 1). *)
-(* Notation "x == y" := (equiv x y).
-Notation observation := (@observation R2 R2 _ R2_EqDec _ R2_EqDec _ MyRobots multiset_observation).
-Notation robogram := (@robogram R2 R2 _ _ _ _ _ MyRobots _).
-Notation configuration := (@configuration R2 _).
-Notation config_list := (@config_list R2 _).
-Notation round := (@round R2 R2 _ _ _ _ _ _ _ _).
-Notation execution := (@execution R2 _). *)
 Notation Madd := (MMultisetInterface.add).
 
 Implicit Type config : configuration.
@@ -252,18 +236,14 @@ intros f s. apply map_injective_support.
 Qed.
 
 
-(* Notation " '!!' '(' config ',' st ')'" :=
-  (fst (@obs_from_config _ _ _ _ (@WithMultiplicityLight.Obs _ _ _ _ _ _) config st )) (at level 10). *)
 Notation " '!!' config" :=
   (@obs_from_config (location * L) _ St _ multiset_observation config (origin, witness)) (at level 10): pactole_scope.
-
 Notation " '!!!' '(' config ',' st ')'" :=
   (@obs_from_config (location * L) _ St _ (@WithMultiplicityLight.Obs _ _ _) config st)  (at level 10): pactole_scope.
 
 Local Open Scope pactole_scope.
 
 
-
 Definition is_black (c:configuration) id :=  get_light (c id) == false.
 Definition is_white (c:configuration) id :=  get_light (c id) == true.
 
@@ -278,7 +258,7 @@ Definition all_active_are_black c da := all_are_black_in c (active da).
 
 Lemma all_active_are_black_equiv : forall config da,
   all_active_are_black config da <-> forall id, activate da id = true -> is_black config id.
-Proof.
+Proof using .
 intros config da.
 unfold all_active_are_black, all_are_black_in.
 rewrite Forall_forall. setoid_rewrite active_spec.
@@ -286,13 +266,13 @@ reflexivity.
 Qed.
 
 Lemma black_white: forall c id, ~ is_black c id <-> is_white c id.
-Proof.
+Proof using .
 intros c id.
 split; intro h; destruct (get_light (c id)) eqn:heq; cbn in *; auto; intro; rewrite h in *; try discriminate.
 Qed.
 
 Lemma white_black: forall c id, ~ is_white c id <-> is_black c id.
-Proof.
+Proof using .
 intros c id.
 split;intro h; destruct (get_light (c id)) eqn:heq;
 cbn in *; auto; try (intro; rewrite h in *; try discriminate).
@@ -300,7 +280,7 @@ elim h; auto.
 Qed.
 
 Lemma all_white_black: forall c l, Forall (fun x => ~ (is_black c x)) l <-> all_are_white_in c l.
-Proof.
+Proof using .
   intros c l.
   apply Forall_Permutation_compat;auto.
   repeat intro.
@@ -310,7 +290,7 @@ Qed.
 
 
 Lemma all_black_white: forall c l, Forall (fun x => ~ (is_white c x)) l <-> all_are_black_in c l.
-Proof.
+Proof using .
   intros c l.
   apply Forall_Permutation_compat;auto.
   repeat intro.
@@ -319,44 +299,44 @@ Proof.
 Qed.
 
 Lemma all_white_black_names: forall c, Forall (fun x => ~ (is_black c x)) names <-> all_are_white c.
-Proof.
+Proof using .
   intros c.
   apply all_white_black.
 Qed.
 
 Lemma all_black_white_names: forall c, Forall (fun x => ~ (is_white c x)) names <-> all_are_black c.
-Proof.
+Proof using .
   intros c.
   apply all_black_white.
 Qed.
 
 Lemma all_white_black_active : forall c da,
   Forall (fun x => ~ (is_black c x)) (active da) <-> all_active_are_white c da.
-Proof.
+Proof using .
   intros.
   apply all_white_black.
 Qed.
 
 Lemma all_black_white_active : forall c da,
   Forall (fun x => ~ (is_white c x)) (active da) <-> all_active_are_black c da.
-Proof.
+Proof using .
  intros.
   apply all_black_white.
 Qed.
 
 
 Lemma get_light_dec_1 c: forall x : ident, get_light (c x) == false \/ ~ get_light (c x) == false.
-Proof.
-  intros x. cbn. destruct (get_light (c x)); intuition.
+Proof using .
+clear. intros x. cbn. destruct (get_light (c x)); intuition.
 Qed.
 
 Lemma get_light_dec_2 c: forall x : ident, get_light (c x) == true \/ ~ get_light (c x) == true.
-Proof.
-  intros x. cbn. destruct (get_light (c x)); intuition.
+Proof using .
+clear. intros x. cbn. destruct (get_light (c x)); intuition.
 Qed.
 
 Lemma is_white_dec c: forall x : ident, is_white c x \/ ~ is_white c x.
-Proof.
+Proof using .
   intros x. 
   unfold is_white.
   destruct (get_light (c x));auto.
@@ -365,7 +345,7 @@ Proof.
 Qed.
 
 Lemma is_black_dec c: forall x : ident, is_black c x \/ ~ is_black c x.
-Proof.
+Proof using .
   intros x. 
   unfold is_black.
   destruct (get_light (c x));auto.
@@ -377,14 +357,14 @@ Definition is_white_b (c:configuration) x: bool := get_light (c x).
 Definition is_black_b (c:configuration) x: bool := negb (get_light (c x)).
 
 Lemma is_white_b_spec: forall c x, is_white_b c x == true <-> is_white c x.
-Proof.
+Proof using .
   intros c x. 
   cbn.
   reflexivity.
 Qed.
 
 Lemma is_black_b_spec: forall c x, is_black_b c x == true <-> is_black c x.
-Proof.
+Proof using .
   intros c x. 
   cbn.
   unfold is_black_b.
@@ -394,14 +374,14 @@ Qed.
 
 Lemma get_location_dec: forall (c:configuration) x loc,
     get_location (c x) == loc \/ ~ get_location (c x) == loc.
-Proof.
+Proof using .
   intros c x loc.
   destruct (equiv_dec (get_location (c x)) loc);auto.
 Qed.
 
 Lemma get_light_decidable (c:configuration) col :
   forall id, { get_light (c id) == col } + { ~ (get_light (c id) == col) }.
-Proof.
+Proof using .
   intros x. cbn. destruct (get_light (c x)).
   destruct col;auto; try (right;intro abs; discriminate).
   destruct col;auto; try (right;intro abs; discriminate).  
@@ -409,7 +389,7 @@ Defined.
 
 Lemma Forall_decidable_color (c:configuration) l col: 
   Decidable.decidable (Forall (fun id0 : ident => get_light (c id0) == col) l).
-Proof.
+Proof using .
   red.
   edestruct (Forall_dec (fun id0 : ident => get_light (c id0) == col) (get_light_decidable c col) l).
   - left;auto. 
@@ -417,39 +397,39 @@ Proof.
 Qed.
 
 Lemma Forall_decidable_black_in c l: Decidable.decidable (all_are_black_in c l).
-Proof.
+Proof using .
   red.
   apply Forall_decidable_color.
 Qed.
 
 Lemma Forall_decidable_white_in c l: Decidable.decidable (all_are_white_in c l).
-Proof.
+Proof using .
   red.
   apply Forall_decidable_color.
 Qed.
 
 Lemma Forall_decidable_black c: Decidable.decidable (all_are_black c).
-Proof.
+Proof using .
   red.
   apply Forall_decidable_color.
 Qed.
 
 Lemma Forall_decidable_white c: Decidable.decidable (all_are_white c).
-Proof.
+Proof using .
   red.
   apply Forall_decidable_color.
 Qed.
 
 
 Lemma Forall_decidable_active_color_black c l: Decidable.decidable (all_active_are_black c l).
-Proof.
+Proof using .
   red.
   apply Forall_decidable_color.
 Qed.
 
 
 Lemma Forall_decidable_active_color_white c l: Decidable.decidable (all_active_are_white c l).
-Proof.
+Proof using .
   red.
   apply Forall_decidable_color.
 Qed.
@@ -473,14 +453,14 @@ Definition is_moving r da c id := List.In id (moving r da c).
 Definition is_stationary r da c id := List.In id (stationary r da c).
 
 Lemma is_moving_dec r da c id: is_moving r da c id \/ ~ is_moving r da c id.
-Proof. destruct (moving_dec r da c id); intuition. Qed.
+Proof using . destruct (moving_dec r da c id); intuition. Qed.
 
 Lemma is_stationary_dec r da c id: is_stationary r da c id \/ ~ is_stationary r da c id.
-Proof. destruct (stationary_dec r da c id); intuition. Qed.
+Proof using . destruct (stationary_dec r da c id); intuition. Qed.
 
 Lemma stationary_moving: forall r da config id,
     ~ is_moving r da config id -> is_stationary r da config id.
-Proof.
+Proof using .
   intros r da config id H. 
   unfold is_moving , is_stationary , stationary, moving in *.
   rewrite List.filter_In in *.
@@ -509,7 +489,7 @@ Lemma bivalent_same_location_2 :
       get_location (config id2)  = pt2 -> 
       get_location (config id3)  = pt3 -> 
       pt1 =/= pt3 -> pt2 =/= pt3 -> pt1 == pt2.
-Proof.
+Proof using .
   intros Loc0 Lght0 VS0 Hnames config pt1 pt2 pt3 id1 id2 id3 H H0 H1 H2 H3 H4. 
   repeat match goal with
     | H: get_location (config ?id) = ?pt |- _ =>
@@ -562,7 +542,7 @@ Definition color_bivalent_on config (pt1 pt2 : location) :=
 
 Lemma count_if_multiplicity: forall config pt,
     count_if (fun id : ident => get_location (config id) ==b pt) = ((!! config)[pt]).
-Proof.
+Proof using .
   intros config pt.
   unfold count_if.
   setoid_rewrite (obs_from_config_fst_ok (origin,witness)(origin,witness)).
@@ -628,8 +608,6 @@ Proof using.
       destruct h_ex_id2 as [id2 h_id2].
       contradiction h_complement_equiv_location_Setoid_x_x0_.
       apply (h id1 id2);auto.
-      -- now symmetry.
-      -- now symmetry.
     + rewrite <- count_if_multiplicity in h_eq_mult_x_div2_add_,h_eq_mult_x0_div2_add_.
       now rewrite h_eq_mult_x_div2_add_,h_eq_mult_x0_div2_add_.
   - intro Hbivalent_on.
@@ -796,464 +774,46 @@ Proof using .
     destruct (List.filter (fun id : ident => get_location (c id) ==b pt1) names) eqn:h_eq_filter.
     { exfalso.
       inversion h_count_lt. }
-    assert (List.In i (List.filter (fun id : ident => get_location (c id) ==b pt1) names)) as h_In.
-    { rewrite h_eq_filter.
-      now constructor. }
-    exists i.
-    apply List.filter_In in h_In.
-    destruct h_In as [h_In h_i_pt1].
-    rewrite equiv_decb_spec in h_i_pt1.
-    rewrite h_i_pt1,h1.
-    assumption.
-Qed.
-
-Lemma count_if_multiplicity_light: forall (config:configuration) (a:location) (col:L) ,
-    count_if (fun id : ident => get_light_decb config col id && R2dec_bool (get_location (config id)) a)
-    = (colors (snd (obs_from_config config (0%VS, witness))))[(a, col)].
-Proof.
-  changeR2.
-  intros config a col.
-  unfold count_if.
-  unshelve setoid_rewrite obs_from_ok.
-  changeR2.
-  cbn [snd].
-  
-  specialize obs_from_config_spec.
-  intros h. 
-  cbn -[names equiv equiv_dec get_location config_list] in h.
-  specialize (h config (a,col)).
-  destruct h as [h1 [h2 h3]].
-  changeR2.
-  rewrite h3.
-  rewrite count_filter_length.
-  rewrite config_list_spec.
-  rewrite filter_map.
-  rewrite map_length.
-  f_equal.
-  apply filter_ext.
-  intros a0. 
-  unfold R2dec_bool.
-  unfold get_light_decb.
-  repeat destruct_match;auto; cbn in *; intuition.
-Qed.
-(*
-Lemma color_bivalent_iff config: color_bivalent config <-> exists pt1 pt2, color_bivalent_on config pt1 pt2.
-Proof.
-Proof.
-  specialize nB_eq_0 as h_nB_0.
-  unfold bivalent_on. split.
-  - intro Hbivalent.
-    specialize (color_bivalent_bivalent Hbivalent) as h_simplbiv.
-    remember Hbivalent as HBiv.
-    clear HeqHBiv.
-    red in Hbivalent.
-    decompose [ex and] Hbivalent /n; clear Hbivalent.
-    exists x, x0.
-    repeat split.
-    + assumption.
-    + intros id.
-      destruct (get_location_dec config id x);auto.
-      destruct (get_location_dec config id x0);auto.
-      exfalso.
-      specialize (@bivalent_same_location_2 _ _ _ _ config x x0 (get_location (config id))) with (id3:=id) as h.
-      assert (0 < Nat.div2 (nG + nB)).
-      { apply Exp_prop.div2_not_R0.
-        lia. }
-      assert (exists id1, get_location (config id1) == x) as h_ex_id1.
-      { apply (obs_from_config_In config (origin,witness)).
-        red.
-        changeR2.
-        rewrite h_eq_mult_x_div2_add_.
-        lia. }
-      assert (exists id2, get_location (config id2) == x0) as h_ex_id2.
-      { apply (obs_from_config_In config (origin,witness)).
-        red.
-        changeR2.
-        rewrite h_eq_mult_x0_div2_add_.
-        lia. }
-      destruct h_ex_id1 as [id1 h_id1].
-      destruct h_ex_id2 as [id2 h_id2].
-      contradiction h_complement_equiv_location_Setoid_x_x0_.
-      apply (h id1 id2);auto.
-      -- now symmetry.
-      -- now symmetry.
-    + rewrite <- count_if_multiplicity in  h_eq_mult_x_div2_add_,h_eq_mult_x0_div2_add_.
-      now rewrite h_eq_mult_x_div2_add_,h_eq_mult_x0_div2_add_.
-    + intros col.
-      rewrite 2 count_if_multiplicity_light.
-      rewrite Forall_forall in h_Forall_l_list_Lght_.
-      apply h_Forall_l_list_Lght_.
-      apply InA_Leibniz.
-      change eq with (@equiv L L_Setoid).
-      apply L_list_InA.
-
-  - intro Hbivalent_on.
-    unfold color_bivalent_on in Hbivalent_on.
-    unfold color_bivalent.
-
-    decompose [and ex] Hbivalent_on /n; clear Hbivalent_on.
-
-Admitted.
-*)    
-(*
-    match type of h_all_eq_count_if_count_if_ with
-      context [count_if (fun id => ?X)] => 
-        idtac
-        (* set (is_notlocx := (fun loc (id : ident) => negb (R2dec_bool a b))) in * *)
-    end.
-    match type of h_eq_count_if_count_if_ with
-      _ = count_if (fun id => R2dec_bool ?a' ?b') => 
-        set (is_notlocx0 := (fun id : ident => negb (R2dec_bool a' b'))) in *
-    end.
-    match type of h_eq_count_if_count_if_ with
-      count_if ?f = count_if ?g => set (is_locx := f) in *; set (is_locx0 := g) in *
-    end.
-
-    assert (forall x1 : ident, is_notlocx x1 = true -> is_locx0 x1 = true) as h_biv.
-    { intros x1 h.
-      destruct (h_all_or_eq_eq_ x1) as [h'|h'];auto.
-      - unfold is_notlocx in h.
-        rewrite negb_true_iff,R2dec_bool_false_iff in h.
-        contradiction.
-      - unfold is_locx0.
-        now rewrite R2dec_bool_true_iff. }
-    assert (forall x1 : ident, is_locx0 x1 = true -> is_notlocx x1 = true).
-    { intros x1 h. 
-      destruct (h_all_or_eq_eq_ x1) as [h'|h'];auto.
-      - unfold is_locx0 in h.
-        rewrite R2dec_bool_true_iff in h.
-        rewrite h' in h.
-        contradiction.
-      - unfold is_notlocx.
-        rewrite negb_true_iff,R2dec_bool_false_iff.
-        now rewrite h'. }
-
-    assert (PermutationA equiv names (List.filter is_locx names ++ (List.filter is_notlocx names))) as h_permut.
-    { transitivity ((fst (List.partition is_locx names) ++ snd (List.partition is_locx names))).
-      - symmetry.
-        apply partition_PermutationA.
-      - apply eqlistA_PermutationA.
-        apply eqlistA_app; try typeclasses eauto.
-        * rewrite Preliminary.partition_filter.
-          reflexivity.
-        * rewrite Preliminary.partition_filter.
-          reflexivity. }
-          
-    assert (PermutationA equiv (List.filter is_notlocx names)
-                               (List.filter is_locx0 (List.filter is_notlocx names)
-                                ++ (List.filter is_notlocx0 (List.filter is_notlocx names)))) as h_permut_nest.
-    { transitivity ((fst (List.partition is_locx0 (List.filter is_notlocx names))
-                    ++ snd (List.partition is_locx0 (List.filter is_notlocx names)))).
-      - symmetry.
-        apply partition_PermutationA.
-      - apply eqlistA_PermutationA.
-        apply eqlistA_app; try typeclasses eauto.
-        * rewrite Preliminary.partition_filter.
-          reflexivity.
-        * rewrite Preliminary.partition_filter.
-          reflexivity. }
-    
-    assert ((List.filter is_notlocx0 (List.filter is_notlocx names)) = nil) as h_nil.
-    { destruct (List.filter is_notlocx0 (List.filter is_notlocx names)) eqn:heq;auto.
-      exfalso.
-      assert (InA equiv i (List.filter is_notlocx0 (List.filter is_notlocx names))) as h.
-      { rewrite heq.
-        apply InA_cons_hd;auto. }
-      rewrite filter_InA in h.
-      destruct h as [h_in h_isnotloc_x0].
-      rewrite filter_InA in h_in.
-      destruct h_in as [ _ h_isnotloc_x].
-      destruct (h_all_or_eq_eq_ i).
-      - unfold is_notlocx in h_isnotloc_x.
-        rewrite negb_true_iff,R2dec_bool_false_iff in h_isnotloc_x.
-        contradiction.
-      - unfold is_notlocx0 in h_isnotloc_x0.
-        rewrite negb_true_iff,R2dec_bool_false_iff in h_isnotloc_x0.
-        contradiction.
-      - typeclasses eauto.
-      - typeclasses eauto. }
-    assert ((!! config)[x] = (!! config)[x0]) as h_mult_eq.
-    { unfold is_locx in h_eq_count_if_count_if_.
-      rewrite count_if_multiplicity in h_eq_count_if_count_if_.
-      unfold is_locx0 in h_eq_count_if_count_if_.
-      rewrite count_if_multiplicity in h_eq_count_if_count_if_.
-      assumption. }
-
-    rewrite h_permut_nest in h_permut.
-    rewrite h_nil in h_permut.
-    clear h_nil h_permut_nest.
-    rewrite app_nil_r in h_permut.      
-    apply PermutationA_length in h_permut.
-    rewrite names_length in h_permut.
-    rewrite app_length in h_permut.
-    rewrite ListComplements.filter_comm in h_permut.
-    rewrite filter_weakened in h_permut;auto.
-
-    red.
-    repeat split.
-    + unfold count_if in h_eq_count_if_count_if_.
-      rewrite h_eq_count_if_count_if_ in h_permut.
-      rewrite h_permut.
-      red.
-      exists (length (List.filter is_locx0 names));lia.
-    + apply le_2_n.
-    + changeR2.
-      exists x, x0.
-      rewrite <- h_mult_eq.
-      rewrite <- count_if_multiplicity.
-      fold is_locx.
-      unfold count_if.
-
-      repeat split.
-      * assumption.
-      * unfold count_if in h_eq_count_if_count_if_.
-        rewrite <- h_eq_count_if_count_if_ in h_permut.
-        rewrite h_permut.
-        match goal  with
-          |- _ = Nat.div2 (?a + ?a) => replace (a + a) with (2 * a)
-        end.
-        -- now rewrite div2_double.
-        -- lia.
-      * unfold count_if in h_eq_count_if_count_if_.
-        rewrite <- h_eq_count_if_count_if_ in h_permut.
-        rewrite h_permut.
-        match goal  with
-          |- _ = Nat.div2 (?a + ?a) => replace (a + a) with (2 * a)
-        end.
-        -- now rewrite div2_double.
-        -- lia.
-  split.
-  - intro Hcolbivalent.
-    specialize (color_bivalent_bivalent Hcolbivalent) as Hbivalent.
-    rewrite bivalent_iff in Hbivalent.
-    destruct Hbivalent as [pt1 [pt2 hbivon]].
-    exists pt1, pt2.
-    split;[assumption|].
-    admit.
-  - intros Hcolbivon.
-    destruct Hcolbivon as [pt1 [pt2 h_colbivon]].
-    unfold color_bivalent_on in h_colbivon.
-    destruct h_colbivon as [h_bivon hcolorsame].
-    assert (bivalent config).
-    { apply bivalent_iff.
-      exists pt1, pt2;auto. }
-    
-
-    red.
-    exists pt1, pt2.
-
-    repeat split;auto.
-    
-
-Admitted.
-*)
-
-(*
-Lemma color_biv_biv config:
-  color_bivalent config <-> 
-    exists pt1 pt2,
-      (bivalent_on config pt1 pt2
-       /\ Forall (fun col : L => (colors (snd (obs_from_config config (0%VS, witness))))[(pt1, col)]
-                                 = (colors (snd (obs_from_config config (0%VS, witness))))[(pt2, col)]) l_list).
-Proof.
-  specialize nB_eq_0 as h_nB_0.
-  unfold bivalent_on. split.
-  - intro Hbivalent.
-    specialize (color_bivalent_bivalent Hbivalent) as h_simplbiv.
-    remember Hbivalent as HBiv.
-    clear HeqHBiv.
-    red in Hbivalent.
-    decompose [ex and] Hbivalent /n; clear Hbivalent.
-    exists x, x0.
-    repeat split.
-    + assumption.
-    + intros id.
-      destruct (get_location_dec config id x);auto.
-      destruct (get_location_dec config id x0);auto.
-      exfalso.
-      specialize (@bivalent_same_location_2 _ _ _ _ config x x0 (get_location (config id)) (id3:=id)) as h.
-      assert (0 < Nat.div2 (nG + nB)).
-      { apply Exp_prop.div2_not_R0.
-        lia. }
-      assert (exists id1, get_location (config id1) == x) as h_ex_id1.
-      { apply (obs_from_config_In config (origin,witness)).
-        red.
-        changeR2.
-        rewrite h_eq_mult_x_div2_add_.
-        lia. }
-      assert (exists id2, get_location (config id2) == x0) as h_ex_id2.
-      { apply (obs_from_config_In config (origin,witness)).
-        red.
-        changeR2.
-        rewrite h_eq_mult_x0_div2_add_.
-        lia. }
-      destruct h_ex_id1 as [id1 h_id1].
-      destruct h_ex_id2 as [id2 h_id2].
-      contradiction h_complement_equiv_location_Setoid_x_x0_.
-      apply (h id1 id2);auto.
-      -- now symmetry.
-      -- now symmetry.
-    + changeR2.
-      rewrite <- count_if_multiplicity in  h_eq_mult_x_div2_add_,h_eq_mult_x0_div2_add_.
-      now rewrite h_eq_mult_x_div2_add_,h_eq_mult_x0_div2_add_.
-    + 
-  - intro Hbivalent_on.
-    decompose [and ex] Hbivalent_on /n; clear Hbivalent_on.
-    match type of h_eq_count_if_count_if_ with
-      count_if (fun id => R2dec_bool ?a ?b) = _ => 
-        set (is_notlocx := (fun id : ident => negb (R2dec_bool a b))) in *
-    end.
-    match type of h_eq_count_if_count_if_ with
-      _ = count_if (fun id => R2dec_bool ?a' ?b') => 
-        set (is_notlocx0 := (fun id : ident => negb (R2dec_bool a' b'))) in *
-    end.
-    match type of h_eq_count_if_count_if_ with
-      count_if ?f = count_if ?g => set (is_locx := f) in *; set (is_locx0 := g) in *
-    end.
-
-    assert (forall x1 : ident, is_notlocx x1 = true -> is_locx0 x1 = true) as h_biv.
-    { intros x1 h.
-      destruct (h_all_or_eq_eq_ x1) as [h'|h'];auto.
-      - unfold is_notlocx in h.
-        rewrite negb_true_iff,R2dec_bool_false_iff in h.
-        contradiction.
-      - unfold is_locx0.
-        now rewrite R2dec_bool_true_iff. }
-    assert (forall x1 : ident, is_locx0 x1 = true -> is_notlocx x1 = true).
-    { intros x1 h. 
-      destruct (h_all_or_eq_eq_ x1) as [h'|h'];auto.
-      - unfold is_locx0 in h.
-        rewrite R2dec_bool_true_iff in h.
-        rewrite h' in h.
-        contradiction.
-      - unfold is_notlocx.
-        rewrite negb_true_iff,R2dec_bool_false_iff.
-        now rewrite h'. }
-
-    assert (PermutationA equiv names (List.filter is_locx names ++ (List.filter is_notlocx names))) as h_permut.
-    { transitivity ((fst (List.partition is_locx names) ++ snd (List.partition is_locx names))).
-      - symmetry.
-        apply partition_PermutationA.
-      - apply eqlistA_PermutationA.
-        apply eqlistA_app; try typeclasses eauto.
-        * rewrite Preliminary.partition_filter.
-          reflexivity.
-        * rewrite Preliminary.partition_filter.
-          reflexivity. }
-          
-    assert (PermutationA equiv (List.filter is_notlocx names)
-                               (List.filter is_locx0 (List.filter is_notlocx names)
-                                ++ (List.filter is_notlocx0 (List.filter is_notlocx names)))) as h_permut_nest.
-    { transitivity ((fst (List.partition is_locx0 (List.filter is_notlocx names))
-                    ++ snd (List.partition is_locx0 (List.filter is_notlocx names)))).
-      - symmetry.
-        apply partition_PermutationA.
-      - apply eqlistA_PermutationA.
-        apply eqlistA_app; try typeclasses eauto.
-        * rewrite Preliminary.partition_filter.
-          reflexivity.
-        * rewrite Preliminary.partition_filter.
-          reflexivity. }
-    
-    assert ((List.filter is_notlocx0 (List.filter is_notlocx names)) = nil) as h_nil.
-    { destruct (List.filter is_notlocx0 (List.filter is_notlocx names)) eqn:heq;auto.
-      exfalso.
-      assert (InA equiv i (List.filter is_notlocx0 (List.filter is_notlocx names))) as h.
-      { rewrite heq.
-        apply InA_cons_hd;auto. }
-      rewrite filter_InA in h.
-      destruct h as [h_in h_isnotloc_x0].
-      rewrite filter_InA in h_in.
-      destruct h_in as [ _ h_isnotloc_x].
-      destruct (h_all_or_eq_eq_ i).
-      - unfold is_notlocx in h_isnotloc_x.
-        rewrite negb_true_iff,R2dec_bool_false_iff in h_isnotloc_x.
-        contradiction.
-      - unfold is_notlocx0 in h_isnotloc_x0.
-        rewrite negb_true_iff,R2dec_bool_false_iff in h_isnotloc_x0.
-        contradiction.
-      - typeclasses eauto.
-      - typeclasses eauto. }
-    assert ((!! config)[x] = (!! config)[x0]) as h_mult_eq.
-    { unfold is_locx in h_eq_count_if_count_if_.
-      rewrite count_if_multiplicity in h_eq_count_if_count_if_.
-      unfold is_locx0 in h_eq_count_if_count_if_.
-      rewrite count_if_multiplicity in h_eq_count_if_count_if_.
-      assumption. }
-
-    rewrite h_permut_nest in h_permut.
-    rewrite h_nil in h_permut.
-    clear h_nil h_permut_nest.
-    rewrite app_nil_r in h_permut.      
-    apply PermutationA_length in h_permut.
-    rewrite names_length in h_permut.
-    rewrite app_length in h_permut.
-    rewrite ListComplements.filter_comm in h_permut.
-    rewrite filter_weakened in h_permut;auto.
-
-    red.
-    repeat split.
-    + unfold count_if in h_eq_count_if_count_if_.
-      rewrite h_eq_count_if_count_if_ in h_permut.
-      rewrite h_permut.
-      red.
-      exists (length (List.filter is_locx0 names));lia.
-    + apply le_2_n.
-    + changeR2.
-      exists x, x0.
-      rewrite <- h_mult_eq.
-      rewrite <- count_if_multiplicity.
-      fold is_locx.
-      unfold count_if.
-
-      repeat split.
-      * assumption.
-      * unfold count_if in h_eq_count_if_count_if_.
-        rewrite <- h_eq_count_if_count_if_ in h_permut.
-        rewrite h_permut.
-        match goal  with
-          |- _ = Nat.div2 (?a + ?a) => replace (a + a) with (2 * a)
-        end.
-        -- now rewrite div2_double.
-        -- lia.
-      * unfold count_if in h_eq_count_if_count_if_.
-        rewrite <- h_eq_count_if_count_if_ in h_permut.
-        rewrite h_permut.
-        match goal  with
-          |- _ = Nat.div2 (?a + ?a) => replace (a + a) with (2 * a)
-        end.
-        -- now rewrite div2_double.
-        -- lia.
-  split.
-  - intros hcolbiv.
-    red in hcolbiv.
-    unfold bivalent_on.
-
-    destruct hcolbiv as [heven [hgt2 [pt1 [pt2 [hneq [hobs1 [hobs2 h_samecol]]]]]]].
-    exists pt1, pt2.
-    split.
-    + 
-    
-
-    remember hcolbiv as hbiv.
-    clear Heqhbiv.
-
+    assert (List.In i (List.filter (fun id : ident => get_location (c id) ==b pt1) names)) as h_In.
+    { rewrite h_eq_filter.
+      now constructor. }
+    exists i.
+    apply List.filter_In in h_In.
+    destruct h_In as [h_In h_i_pt1].
+    rewrite equiv_decb_spec in h_i_pt1.
+    rewrite h_i_pt1,h1.
+    assumption.
+Qed.
 
-    apply color_bivalent_bivalent in hbiv.
-    apply bivalent_iff in hbiv.
-    unfold color_bivalent in *.
-    
-    destruct hcolbiv as [heven [hgt2 [pt1 [pt2 [hneq [hobs1 [hobs2 h_samecol]]]]]]].
-    exists pt1, pt2.
-    split.
-    + assert (bivalent config).
-      { red.
-        repeat split;auto.
-        exists pt1, pt2;auto. }
-      apply bivalent_iff.
-    
+Lemma count_if_multiplicity_light: forall (config:configuration) (a:location) (col:L) ,
+    count_if (fun id : ident => get_light_decb config col id && R2dec_bool (get_location (config id)) a)
+    = (colors (snd (obs_from_config config (0%VS, witness))))[(a, col)].
+Proof using .
+  changeR2.
+  intros config a col.
+  unfold count_if.
+  unshelve setoid_rewrite obs_from_ok.
+  changeR2.
+  cbn [snd].
+  
+  specialize obs_from_config_spec.
+  intros h. 
+  cbn -[names equiv equiv_dec get_location config_list] in h.
+  specialize (h config (a,col)).
+  destruct h as [h1 [h2 h3]].
+  changeR2.
+  rewrite h3.
+  rewrite count_filter_length.
+  rewrite config_list_spec.
+  rewrite filter_map.
+  rewrite map_length.
+  f_equal.
+  apply filter_ext.
+  intros a0. 
+  unfold R2dec_bool.
+  unfold get_light_decb.
+  repeat destruct_match;auto; cbn in *; intuition.
 Qed.
-*)
 
 (** Observations can never be empty as the number of robots is non null. *)
 
@@ -1297,7 +857,7 @@ intros pt config. etransitivity.
 Qed.
 
 Lemma obs_from_ok: forall config st, (!!!(config,st)) == (!! config, snd (!!!(config,st))).
-Proof.
+Proof using .
   intros config st. 
   specialize (obs_from_config_ignore_snd_except_observerlight st config st) as h.
   lazy zeta in h.
@@ -1452,7 +1012,7 @@ Definition find_max_black (obs : (@observation (location * L) _ _ _ Obs)) loc1 l
   if Nat.leb col1 col2 then loc2 else loc1.
 
 Instance find_max_black_compat: Proper (@equiv observation _ ==> equiv ==> equiv ==> equiv) find_max_black.
-Proof.
+Proof using .
 intros obs1 obs2 Hobs loc1 loc1' Hloc1 loc2 loc2' Hloc2.
 unfold find_max_black.
 now rewrite Hobs, 2 Hloc1, 2 Hloc2.
@@ -1460,155 +1020,14 @@ Qed.
 
 Lemma find_max_black_indep : forall config st1 st2 pt1 pt2,
   find_max_black (!!! (config, st1)) pt1 pt2 == find_max_black (!!! (config, st2)) pt1 pt2.
-Proof.
+Proof using .
 intros config st1 st2 pt1 pt2. unfold find_max_black.
 now rewrite (colors_indep config st1 st2).
 Qed.
 
 Lemma find_max_black_either : forall obs pt1 pt2,
   find_max_black obs pt1 pt2 == pt1 \/ find_max_black obs pt1 pt2 == pt2.
-Proof. intros. unfold find_max_black. destruct_match; now left + right. Qed.
-
-
-(*
-(* Find the tower with the most black robots in bivalent configurations if it is unique. *)
-Definition find_blackest_tower (obs : observation) : location :=
-  match support (fst obs) with
-    | pt1 :: pt2 :: nil =>
-        let col1 := (colors (snd obs))[(pt1, false)] in
-        let col2 := (colors (snd obs))[(pt2, false)] in
-        if Nat.ltb col1 col2 then pt2 else
-        if Nat.ltb col2 col1 then pt1 else middle pt1 pt2
-    | _ => origin (* dummy case *)
-  end.
-
-Instance find_blackest_tower_compat : Proper (@equiv observation _ ==> equiv) find_blackest_tower.
-Proof.
-intros obs1 obs2 Hobs. unfold find_blackest_tower.
-assert (Hperm := support_compat (fst_compat_pactole Hobs)).
-assert (Hlen := PermutationA_length Hperm).
-destruct (support (fst obs1)) as [| pt1 [| pt2 []]],
-         (support (fst obs2)) as [| pt1' [| pt2' []]];
-cbn in Hlen; try discriminate || reflexivity; [].
-rewrite PermutationA_2 in Hperm; auto; [].
-destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]]; rewrite Heq1, Heq2, Hobs.
-+ now do 2 (destruct_match; assumption || rewrite Heq1, Heq2, ?Hobs).
-+ repeat (destruct_match; assumption || rewrite ?Heq1, ?Heq2, ?Hobs); try reflexivity; [|].
-  - exfalso. rewrite Nat.ltb_lt in *. lia.
-  - apply middle_comm.
-Qed.
-
-Lemma find_blackest_tower_morph : forall f obs,
-  bivalent_obs obs = true -> color_bivalent_obs obs = false ->
-  find_blackest_tower (map_obs f obs) == f (find_blackest_tower obs).
-Proof.
-intros f obs Hbivalent Hcolor. unfold find_blackest_tower, map_obs. cbn [fst snd].
-assert (Hperm := map_sim_support_fst f obs).
-assert (Hbiv := Hbivalent).
-apply bivalent_obs_support in Hbiv.
-changeR2.
-lazymatch goal with
-  |- match ?x with _ => _ end == Bijection.section f (match ?y with _ => _ end) =>
-    assert (Hlen : length x = length y) by (now rewrite Hperm, map_length);
-    destruct x as [| pt1' [| pt2' []]],
-             y as [| pt1 [| pt2 []]] eqn:Hcase; cbn in Hlen; try discriminate; clear Hlen
-end.
-apply PermutationA_2 in Hperm; autoclass; [].
-destruct Hperm as [[Heq1 Heq2] | [Heq1 Heq2]];
-repeat first [ assumption
-             | eelim lt_irrefl; etransitivity; eassumption
-             | progress rewrite ?Nat.ltb_lt, ?Nat.ltb_nlt in *
-             | rewrite Heq1, Heq2, 2 (map_light_colors _ (Bijection.injective f) (snd obs))
-             | destruct_match ].
-* contradict Hcolor. rewrite not_false_iff_true.
-  unfold bivalent_obs, color_bivalent_obs in *. changeR2. rewrite Hcase in *.
-  rewrite andb_true_iff, List.forallb_forall in  *. split; trivial; [].
-  intros c _. rewrite Nat.eqb_eq. destruct c.
-  + 
-  + lia.
-  unfold bivalent_obs in Hbivalent. rewrite
-Qed.
-
-Lemma find_blackest_tower_spec : forall config,
-  bivalent config -> ~color_bivalent config ->
-  forall st pt, let obs := !!!(config, st) in
-  ((colors (snd obs))[(pt, false)] < (colors (snd obs))[(find_blackest_tower obs, false)])%nat.
-Proof.
-intros config Hbivalent Hcolor st pt. cbn.
-assert (Hlen := bivalent_support st Hbivalent).
-apply biv_col_obs_indep in Hcolor.
-unfold find_blackest_tower. color_bivalent_obs
-Qed.
-
-(* Find the towers with the most black robots. *)
-
-Local Definition get_max_black (x : location * L) k acc :=
-  if Bool.eqb (snd x) false
-  then match Nat.compare k (fst acc) with
-         | Eq => (fst acc, (fst x) :: (snd acc))
-         | Gt => (k, (fst x) :: nil)
-         | Lt => acc
-       end
-  else acc.
-
-Instance get_max_black_compat :
-  Proper (equiv ==> eq ==> equiv * PermutationA equiv ==> equiv * PermutationA equiv) get_max_black.
-Proof.
-unfold get_max_black.
-intros [pt1 c1] [pt2 c2] [Hpt Hc] pp p ? acc1 acc2 Hacc.
-subst pp. cbn [fst snd] in *. rewrite Hc, Hacc.
-destruct (eqb_spec c2 false), (Nat.compare_spec p (fst acc2)); trivial; [|].
-- split; try apply Hacc; []. hnf; cbn [snd]. constructor; trivial; apply Hacc.
-- now rewrite Hpt.
-Qed.
-
-Lemma get_max_black_transpose :
-  Preliminary.transpose2 (equiv * PermutationA equiv)%signature get_max_black.
-Proof.
-intros x y m p acc. unfold get_max_black.
-repeat destruct_match; split; cbn in *; reflexivity || congruence || auto;
-rewrite ?Nat.compare_eq_iff, ?Nat.compare_lt_iff, ?Nat.compare_gt_iff in *;
-reflexivity || congruence || (now constructor) || lia.
-Qed.
-
-Definition find_blackest_towers (obs : obsLight) : nat * list location :=
-  fold get_max_black (colors obs) (0%nat, nil).
-
-Instance find_blackest_towers_compat :
-  Proper (equiv ==> equiv * PermutationA equiv) find_blackest_towers.
-Proof.
-intros obs1 obs2 Hobs. unfold find_blackest_towers.
-apply fold_compat; autoclass.
-+ apply get_max_black_transpose.
-+ now rewrite Hobs.
-+ reflexivity.
-Qed.
-
-Lemma find_blackest_towers_morph : forall (f : Bijection.bijection location) obs,
-  (equiv * PermutationA equiv)%signature (find_blackest_towers (map_light f obs))
-  (fst (find_blackest_towers obs), List.map f (snd (find_blackest_towers obs))).
-Proof.
-intros f obs. unfold find_blackest_towers.
-unfold map_light. cbn [colors].
-rewrite (map_injective_fold _ get_max_black_compat get_max_black_transpose).
-* pattern (colors obs). apply ind.
-  +
-Abort.
-
-Lemma find_blackest_towers_spec : forall obs k l,
-  find_blackest_towers obs = (k, l)
-  <-> forall pt, (InA equiv pt l -> (colors obs)[(pt, false)] = k)
-              /\ (~ InA equiv pt l -> (colors obs)[(pt, false)] < n)%nat.
-Proof.
-intros obs k l. split.
-* (* Correctness *)
-  intros Hobs pt. split.
-  + (* A blackest tower *)
-    intro Hpt.
-  + 
-* (* Completeness *)
-Qed.
-*)
+Proof using . intros. unfold find_max_black. destruct_match; now left + right. Qed.
 
 Definition find_other_loc obs (loc : location) :=
   match support obs with
@@ -1619,7 +1038,7 @@ Definition find_other_loc obs (loc : location) :=
   end.
 
 Instance find_other_loc_compat : Proper (equiv ==> equiv ==> equiv) find_other_loc.
-Proof.
+Proof using .
 intros obs1 obs2 Hobs loc1 loc2 Hloc. unfold find_other_loc.
 assert (Hperm : PermutationA equiv (support obs1) (support obs2)).
 { apply support_compat, Hobs. }
@@ -1640,7 +1059,7 @@ Qed.
 Lemma find_other_loc_spec : forall obs, bivalent_obs obs = true ->
   forall pt, In pt (fst obs) ->
   PermutationA equiv (support (fst obs)) (pt :: find_other_loc (fst obs) pt :: nil).
-Proof.
+Proof using .
 intros obs Hbivalent pt Hpt. unfold find_other_loc, bivalent_obs in *.
 assert (Hnodup := support_NoDupA (fst obs)).
 destruct obs as [obs1 ?]. cbn [fst] in *.
@@ -1656,7 +1075,7 @@ Qed.
 
 Corollary find_other_loc_diff : forall obs, bivalent_obs obs = true ->
   forall pt, In pt (fst obs) -> @complement _ (@equiv _ location_Setoid) (find_other_loc (fst obs) pt) pt.
-Proof.
+Proof using .
 intros obs Hobs pt Hperm. apply find_other_loc_spec in Hperm; trivial; [].
 assert (Hnodup := support_NoDupA (fst obs)).
 rewrite Hperm in Hnodup. inv Hnodup.
@@ -1665,7 +1084,7 @@ Qed.
 
 Corollary find_other_loc_In : forall obs, bivalent_obs obs = true ->
   forall pt, In pt (fst obs) -> In (find_other_loc (fst obs) pt) (fst obs).
-Proof.
+Proof using .
 intros obs Hbivalent pt Hin.
 apply find_other_loc_spec in Hin; trivial; [].
 rewrite <- support_spec, Hin. now right; left.
@@ -1684,16 +1103,8 @@ Definition gatherR2_pgmLight (obs : observation) : location * L :=
             (maj_black, observer_lght (snd obs))
   else (gatherR2_old_pgm (fst obs), observer_lght (snd obs)).
 
-
-(*
-Ltac absurd_lgth h :=
-  apply PermutationA_length in h;
-  cbn in h;
-  inversion h.
-*)
-
 Global Instance gatherR2_pgmLight_compat: Proper (equiv ==> equiv) gatherR2_pgmLight.
-Proof.
+Proof using size_G.
 intros obs1 obs2 Hobs. unfold gatherR2_pgmLight.
 repeat first [ reflexivity | setoid_rewrite Hobs | destruct_match].
 Qed.
@@ -1928,8 +1339,6 @@ unfold no_Majority. split.
     (!! config)[pt0] = Nat.div2 (nG+nB) /\ (!! config)[pt3] = Nat.div2 (nG+nB) /\ Nat.Even (nG+nB)).
   { intros h.
     decompose [ex and] h; repeat split; trivial.
-    (* - unfold ge. transitivity 3; lia || apply size_G. *)
-    (* - inversion H3. exists x1;lia. *)
     - unfold ge. cbn. lia.
     - exists x, x0; intuition. }
   exists pt1, pt2.
@@ -2190,7 +1599,7 @@ simpl in Hsize; lia || clear Hsize.
 Qed.
 
 Instance count_black_compat : Proper (equiv ==> Logic.eq) count_black.
-Proof.
+Proof using size_G.
   intros s1 s2 Hs.
   unfold count_black.
   apply fold_compat;autoclass.
@@ -2202,7 +1611,7 @@ Proof.
 Qed.
 
 Instance measure_compat : Proper (equiv ==> Logic.eq) measure.
-Proof.
+Proof using size_G.
   intros s1 s2 Hs. unfold measure.
   rewrite Hs.
   destruct (bivalent_obs s2).
@@ -2307,7 +1716,7 @@ Qed.
 
 Lemma find_other_loc_morph : forall (sim : similarity location) obs pt,
   find_other_loc (map sim obs) (sim pt) == sim (find_other_loc obs pt).
-Proof.
+Proof using n.
 intros sim obs pt. unfold find_other_loc.
 assert (Hperm := map_sim_support sim obs).
 assert (Hlen := PermutationA_length Hperm).
@@ -2333,7 +1742,7 @@ Lemma find_max_black_morph : forall sim : similarity location,
   forall (obs : observation (Observation := Obs)) (pt1 pt2 : location),
     find_max_black (map sim (fst obs), map_light sim (snd obs)) (sim pt1) (sim pt2)
     == sim (find_max_black obs pt1 pt2).
-Proof.
+Proof using .
 intros sim obs pt1 pt2. unfold find_max_black.
 cbn -[equiv]. set (f := fun x : location * L => (sim (fst x), snd x)).
 change (map _ (colors ?A)) with (map f (colors A)).
@@ -2649,7 +2058,6 @@ destruct (existsb (fun x => if get_location (round r da config x) =?= pt then
   { apply obs_from_config_spec. }
   rewrite H ; autoclass; [].
   rewrite H0 ; autoclass; [].
-  (* setoid_rewrite obs_from_config_spec. ; autoclass; []. *)
   do 2 rewrite config_list_spec.
   induction names as [| id l]; trivial; [].
   destruct (get_location (round r da config id) =?= pt) as [Heq | Heq];cbn -[equiv_dec];
@@ -2802,8 +2210,6 @@ unfold local_robot_decision, gatherR2. simpl pgm.
 unfold gatherR2_pgmLight.
 (* Expressing the local observation in terms of the global one. *)
 assert (Hobs : local_obs == (map (sim_f sim) (fst global_obs), map_light (sim_f sim) (snd global_obs))).
-(*              {| observer_lght := observer_lght (snd global_obs);
-                colors := map (fun x => (new_frame (fst x), snd x)) (colors (snd global_obs))|})). *)
 { unfold local_obs, local_state, local_config. unfold map_config at 2.
   now rewrite (WithMultiplicityLight.obs_from_config_map _ Hsim Hinj
                 (precondition_satisfied da config g) config (config (Good g))). }
@@ -3094,7 +2500,6 @@ destruct (get_location (config id) ==b loc_g1) eqn:Hcase; cbn [negb]; reflect_bo
 + 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.
-  apply find_other_loc_diff_here.
 Qed.
 
 
@@ -3184,7 +2589,6 @@ 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.
-  apply find_other_loc_diff_here.
 Qed.
 
 Lemma active_split : PermutationA equiv (active_on_g1 ++ active_on_other) (active da).
@@ -3360,7 +2764,7 @@ rewrite Hobs, Hactive. reflexivity.
 Qed.
 
 Corollary a3b_same_loc : forall id, get_location (round gatherR2 da config id) == get_location (config id).
-Proof. intro id. rewrite (a3b_next_round id). now destruct_match. Qed.
+Proof using Hssync Hcolor Hallblack. intro id. rewrite (a3b_next_round id). now destruct_match. Qed.
 
 Lemma a3b_same_obs : !! (round gatherR2 da config) == !! config.
 Proof using Hssync Hcolor Hallblack.
@@ -3400,7 +2804,7 @@ Qed.
 Corollary a3b_next_black_eqb : forall id,
   get_light (round gatherR2 da config id) ==b false
   = (get_light (config id) ==b false) && negb (activate da id).
-Proof.
+Proof using Hssync Hcolor Hallblack.
 intro id. symmetry.
 destruct (get_light (round gatherR2 da config id)) eqn:Hcase; reflect_bool.
 + rewrite (a3b_next_white id) in Hcase. cbn in *. intuition congruence.
@@ -3410,7 +2814,7 @@ Qed.
 Corollary a3b_next_white_eqb : forall id,
   get_light (round gatherR2 da config id) ==b true
   = (get_light (config id) ==b true) || activate da id.
-Proof.
+Proof using Hssync Hcolor Hallblack.
 intro id. symmetry.
 destruct (get_light (round gatherR2 da config id)) eqn:Hcase; reflect_bool.
 + rewrite (a3b_next_white id) in Hcase. cbn in *. intuition congruence.
@@ -3419,7 +2823,7 @@ Qed.
 
 Lemma state_eqb : forall st1 st2,
   (st1 ==b st2) = (get_location st1 ==b get_location st2) && (get_light st1 ==b get_light st2).
-Proof.
+Proof using .
 intros [pt1 l1] [pt2 l2]. cbn. changeR2.
 destruct (pt1 ==b pt2) eqn:Hpt, (l1 ==b l2) eqn:Hl; reflect_bool; cbn in *; tauto.
 Qed.
@@ -3427,7 +2831,7 @@ Qed.
 Corollary a3b_state_same_eqb : forall id,
   (round gatherR2 da config id ==b config id)
   = (get_light (round gatherR2 da config id) ==b get_light (config id)).
-Proof. intro. rewrite state_eqb, a3b_same_loc. now simpl_bool. Qed.
+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.
@@ -3443,7 +2847,7 @@ Qed.
 
 Lemma a3b_next_black_idle_is_black_idle : forall pt,
   black_idle_on pt (round gatherR2 da config) = black_idle_on pt config.
-Proof.
+Proof using Hssync Hcolor Hallblack.
 intro pt. unfold black_idle_on, idle_on, idle.
 repeat rewrite <- filter_andb. f_equiv.
 intros xx id ?. subst xx.
@@ -3452,7 +2856,7 @@ now destruct (activate da id); simpl_bool.
 Qed.
 
 Lemma a3b_white_idle_is_white : forall pt, white_idle_on pt config = white_on pt config.
-Proof.
+Proof using Hallblack.
 intros pt. unfold light_idle_on, idle_on, idle, white_on, on_loc.
 repeat rewrite <- filter_andb. f_equiv.
 intros xx id ?. subst xx.
@@ -3466,7 +2870,7 @@ Qed.
 
 Lemma a3b_next_white_idle_is_white : forall pt,
   white_idle_on pt (round gatherR2 da config) = white_on pt config.
-Proof.
+Proof using Hssync Hcolor Hallblack.
 intros pt. unfold light_idle_on, idle_on, idle, white_on, on_loc.
 repeat rewrite <- filter_andb. f_equiv.
 intros xx id ?. subst xx.
@@ -3482,7 +2886,7 @@ Qed.
 
 Lemma a3b_length_idle_active : forall pt,
   length (List.filter (fun id => (config id ==b (pt, false)) && negb (activate da id)) (active da)) = 0.
-Proof.
+Proof using .
 intro pt. unfold active. rewrite <- filter_andb.
 induction names; cbn; trivial; [].
 destruct_match; auto; [].
@@ -3492,7 +2896,7 @@ Qed.
 Lemma a3b_length_black_idle : 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.
+Proof using .
 intros pt pt'. unfold black_idle_on, idle_on, idle. repeat rewrite <- filter_andb.
 destruct (pt' ==b pt) eqn:Heq_pt.
 * induction names as [| id l]; cbn; trivial; [].
@@ -3544,30 +2948,10 @@ destruct (Forall_dec (is_black config) Hdec (active da)).
   intros [h1 h2].
   contradiction.
 Qed.
-(*
-Definition cb_cb_precondition :=
-  (* locations of both towers *)
-  exists pt1 pt2, (exists id, get_location (config id) == pt1)
-               /\ (exists id, get_location (config id) == pt2)
-               /\ pt1 =/= pt2
-  (* All active robots are black *)
-  /\ Forall (fun id => get_light (config id) == false) (active da)
-  (* same number of activated robots on each tower *)
-  /\ let (l1,l2) := List.partition ((fun id => equiv_decb (get_location (config id)) pt1)) (active da) in
-      length l1 = length l2
-      /\ Forall (fun id => get_location (config id) == pt2) l2.
-
-    (exists l1 l2, PermutationA equiv (active da) (l1 ++ l2)
-                 /\ Forall (fun id => get_location (config id) == pt1) l1
-                 /\ Forall (fun id => get_location (config id) == pt2) l2
-                 /\ length l1 = length l2).
-*)
 
 Lemma color_bivalent_next_color_bivalent :
   cb_cb_precondition ->
   color_bivalent (round gatherR2 da config).
-(*   /\ count_black (!!! (round gatherR2 da config, round gatherR2 da config (Good g1)))
-     < count_black (!!! (config, config (Good g1))) *)
 Proof using Hssync Hcolor.
 intros [Hactive Hlen].
 assert (Hcol := Hcolor). destruct Hcol as [Heven [Hn [pt1 [pt2 [Hdiff [Hpt1 [Hpt2 Hall]]]]]]].
@@ -3652,9 +3036,6 @@ Qed.
 Definition cb_b_precondition_all_white :=
   (* All robots are white *)
   all_are_white config
-  (* Forall (fun id => get_light (config id) == true) names *)
-  (* TODO: REPLACE BY THIS?: Advantage: we don't use hd and its default value)*)
-  (* /\ (length active_on_g1 = 0 \/ length active_on_other = 0). *)
   /\ active da = on_loc (get_location (config (hd (Good g1) (active da)))) config.
   (* TODO: rename g1 *)
 
@@ -3861,8 +3242,6 @@ Qed.
 Definition cb_b_precondition_only_black_active :=
   (* All active robots are black *)
   all_active_are_black config da
-  (* Forall (fun id => get_light (config id) == false) (active da) *)
-  (* locations of both towers *)
   (* different number of activated robots on each tower *)
   /\ length active_on_g1 <> length active_on_other.
 
@@ -3988,7 +3367,7 @@ 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.
-    apply (bivalent_support (config := config)); auto; []. now symmetry. }
+    apply (bivalent_support (config := config)); auto. }
   rewrite PermutationA_2 in Hperm; auto; [].
   destruct Hperm as [[Heq _] | [Heq _ ]]; rewrite Heq; auto. }
 apply lt_le_trans with (length (moving gatherR2 da config)).
@@ -4039,7 +3418,7 @@ Qed.
 
 
 Lemma forall_ident pred: Forall pred names <-> forall id:ident, pred id.
-Proof.
+Proof using .
   split.
   - intros H id. 
     eapply Forall_forall in H;eauto.
@@ -4051,7 +3430,7 @@ Proof.
 Qed.
 
 Lemma exists_ident pred: List.Exists pred names <-> exists id:ident, pred id.
-Proof.
+Proof using .
   split.
   - intros H. 
     eapply Exists_exists in H;eauto.
@@ -4072,7 +3451,7 @@ Lemma Exists_decidable :
   forall [A : Type] (P : A -> Prop),
     (forall x : A, P x \/ ~ P x)
     -> forall (l : list A), List.Exists P l \/~ List.Exists P l.
-Proof.
+Proof using .
   intros A P H l.
   induction l.
   - right.
@@ -4096,7 +3475,7 @@ Lemma Forall_decidable :
   forall [A : Type] (P : A -> Prop),
     (forall x : A, P x \/ ~ P x)
     -> forall (l : list A), List.Forall P l \/~ List.Forall P l.
-Proof.
+Proof using .
   intros A P H l.
   induction l.
   - left.
@@ -4118,7 +3497,7 @@ Lemma dec1 id1 id:
    is_moving gatherR2 da config id)
   \/ ~ (get_location (config id) == get_location (config id1) ->
         is_moving gatherR2 da config id).
-Proof.
+Proof using .
   destruct (equiv_dec (get_location (config id)) (get_location (config id1))).
   - destruct (in_dec names_eq_dec id (moving gatherR2 da config)).
     + left.
@@ -4137,7 +3516,7 @@ Lemma sub_cb_nb_precondition_wholecolmove_dec id1:
   \/ ~ (forall id : ident,
            get_location (config id) == get_location (config id1) ->
            is_moving gatherR2 da config id).
-Proof.
+Proof using .
   rewrite <- forall_ident.
   match goal with
     |- Forall ?pred _ \/ _ => destruct (Forall_decidable pred (dec1 id1) names)
@@ -4154,7 +3533,7 @@ Lemma dec3 x:
           (forall id : ident,
               get_location (config id) == get_location (config x) ->
               is_moving gatherR2 da config id) /\ is_moving gatherR2 da config id2).
-Proof.
+Proof using .
   red.
   rewrite <- exists_ident.
   apply Exists_decidable.
@@ -4173,7 +3552,7 @@ Qed.
 
 Lemma cb_nb_precondition_wholecolmove_dec: 
   cb_nb_precondition_wholecolmove \/ ~ cb_nb_precondition_wholecolmove .
-Proof.
+Proof using .
   unfold cb_nb_precondition_wholecolmove.
   setoid_rewrite <- exists_ident.
   apply Exists_decidable.
@@ -4184,7 +3563,7 @@ Qed.
 
 Lemma observer_light_get_light: forall id,
     observer_lght (snd (obs_from_config config (config id))) = get_light (config id).
-Proof.
+Proof using .
   intros id.
   reflexivity.
 Qed.
@@ -4194,7 +3573,7 @@ Lemma cb_nb_spec_1:
   cb_nb_precondition_wholecolmove
   -> (exists id_move, is_moving gatherR2 da config id_move)
      /\ ~ Forall (fun id => get_location (config id) == get_location (config (hd (Good g1) (active da)))) (active da).
-Proof.
+Proof using Hssync Hcolor.
   intros h_wholecolmoves.
   unfold cb_nb_precondition_wholecolmove , cb_nb_precondition_somestay in *.
   destruct h_wholecolmoves as [ida [idb [h_diffab [h_colmove_on_ida h_somemove_on_idb]]]].
@@ -4208,7 +3587,7 @@ Proof.
     specialize (h config (get_location (config idb))).
     specialize (h (get_location (config (hd (Good g1) (active da))))).
     specialize (h (get_location (config ida))).
-    eapply h; auto. now symmetry. }
+    eapply h; auto. }
   assert (List.In idb (active da)) as h_acive_idb.
   { eapply moving_active; eauto. }
   
@@ -4228,39 +3607,12 @@ Proof.
     symmetry in abs.
     contradiction.
 Qed.
-(*
-(* cb_someone moves and not extacly one column moves. *)
-Lemma cb_nb_spec:
-  (cb_nb_precondition_somestay)
-  -> (exists id_move, is_moving config da id_move)
-       /\ ~ cb_b_precondition_all_white.
-Proof.
-  intros h_somestay.
-  unfold cb_nb_precondition_wholecolmove , cb_nb_precondition_somestay in *.
-  destruct h_somestay as [id_move2 [idc [idd [h_diff_dicd [h_id_move2 [h_id1_nomoves h_id2_nomoves]]]]]].
-  unfold cb_b_precondition_all_white.
-  rewrite not_and_3;auto with color_dec.
-  2:{ apply dec_eq_nat. }
-  split.
-  { exists id_move2;auto. }
-  right. right.
-  intro abs.
-  assert ((hd (Good g1) (active da)) == idc \/ ((hd (Good g1) (active da)) == idd)).
-  { admit. }
-  destruct H as [h | h].
-  - rewrite h in abs.
-    Forall_forall
-  
-  specialize (abs )
-Qed.
-                      
-*)
 
 (* TODO: functions to extract robots on a given location without using observation
          + thms about splitting and merging configs *)
 
 Lemma black_dont_move: forall id, is_black config id -> is_stationary gatherR2 da config id.
-Proof.
+Proof using Hssync Hcolor.
   intros id H. 
   unfold is_stationary.
   rewrite stationary_iff_not_moving, moving_iff.
@@ -4271,17 +3623,13 @@ Proof.
 Qed.
 
 
-
-
-
-
 Lemma not_false_iff_true_equiv: forall b:bool, ~ (b == false) <-> b == true.
-Proof.
+Proof using .
   destruct b;intros;intuition.
 Qed.
 
 Lemma not_true_iff_false_equiv: forall b:bool, ~ (b == true) <-> b == false.
-Proof.
+Proof using .
   destruct b;intros;intuition.
 Qed.
 
@@ -4326,13 +3674,19 @@ Proof using Hcolor Hssync.
   - now apply (moving_active Hssync gatherR2 config).
 Qed.
 
-
+Lemma ident_eq_decidable: ListDec.decidable_eq ident.
+Proof using.
+  red.
+  intros.
+  red.
+  destruct (names_eq_dec x y);auto.
+Qed.
 
 Lemma color_bivalent_exhaustive_cases :
   cb_cb_precondition
   \/ (cb_b_precondition_all_white \/ cb_b_precondition_only_black_active)
   \/ (cb_nb_precondition_wholecolmove \/ cb_nb_precondition_somestay).
-Proof.
+Proof using Hssync Hcolor.
 destruct (active da) as [| id l] eqn:Hactive.
 - (* No active robot *)
   left.
@@ -4363,34 +3717,6 @@ destruct (active da) as [| id l] eqn:Hactive.
   unfold cb_cb_precondition, cb_b_precondition_all_white,
          cb_b_precondition_only_black_active, cb_nb_precondition_wholecolmove in *.
   rewrite not_and in *; auto with color_dec.
-  
-(*
-  assert ((forall id1 id2 : ident,
-              get_location (config id2) == get_location (config id1) \/
-                (exists id : ident,
-                    get_location (config id) == get_location (config id1) /\
-                      ~ is_moving gatherR2 da config id) \/
-                ~is_moving gatherR2 da config id2)
-          -> ~ (exists id1 id2 : ident,
-                   get_location (config id2) =/= get_location (config id1) /\
-                     (forall id : ident,
-                         get_location (config id) == get_location (config id1)
-                         -> is_moving gatherR2 da config id) /\
-                     is_moving gatherR2 da config id2)).
-{ clear.
-  intros H.
-  intro abs.
-  decompose [ex and] abs; clear abs.
-  specialize (H x x0).
-  
-  decompose [ex and or] H;clear H.
-  - contradiction.
-  - specialize (H1 x1 H4).
-    contradiction.
-  - contradiction. }
-*)
-
-
 
   assert ((forall id1 id2 : ident,
                   get_location (config id2) == get_location (config id1) \/
@@ -4493,13 +3819,12 @@ destruct (active da) as [| id l] eqn:Hactive.
   clear h_cb_nb_wm.
   rename h_cb_nb_wm' into h_cb_nb_wm.
 
-
   red.
   assert (~all_active_are_black config da) as not_all_blacks.
   { destruct h_cb_cb;auto.
     destruct h_cb_b_onlyb;auto. }
   clear h_cb_cb h_cb_b_onlyb.
-  
+
   (* not_all_blacks is enough to have one moving robot *)
   assert (exists id_move, is_moving gatherR2 da config id_move) as hex.
   { unfold all_active_are_black, all_are_black_in in not_all_blacks.
@@ -4511,7 +3836,7 @@ destruct (active da) as [| id l] eqn:Hactive.
       split;auto.
       now apply black_white.
     - apply is_black_dec. }
-  
+
   destruct hex as [id_move hmove].
   exists id_move.
   enough (exists id1 id2 : ident,
@@ -4574,8 +3899,7 @@ destruct (active da) as [| id l] eqn:Hactive.
       * now apply black_dont_move.
       * now apply black_dont_move.
     + assert ((get_location (config id_black) == pt2)) as h_idblack_pt2.
-      { apply bivalent_same_location with (pt3:=pt1) (config:=config) (st:=(0%VS, witness)); auto.
-        now symmetry. }
+      { apply bivalent_same_location with (pt3:=pt1) (config:=config) (st:=(0%VS, witness)); auto. }
       assert (exists id_black2, is_black config id_black2
                                 /\ (get_location (config id_black2) == pt1)) as hex.
       { rewrite Forall_forall in h_samecol.
@@ -4624,8 +3948,6 @@ destruct (active da) as [| id l] eqn:Hactive.
     clear h_cb_b_allw.
     rename h into h_cb_b_allw.
     destruct h_cb_b_allw as [h_not_div2_active | [h_exactly_div2 h_not_all_sameloc]].
-        Set Nested Proofs Allowed.
-
 
     - (* (h_cb_nb_wm idopp) proves that there is a robot id' opposite
          to id_move that does not move. *)
@@ -4642,9 +3964,8 @@ destruct (active da) as [| id l] eqn:Hactive.
           assumption.
         - exfalso.
           specialize (h_forall id_move).
-          apply h_forall;auto.
-          now symmetry. }
-      
+          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
@@ -4681,7 +4002,7 @@ destruct (active da) as [| id l] eqn:Hactive.
           tauto. }
         clear h.
         rewrite Forall_forall in h'.
-        
+
         specialize (h_cb_nb_wm id_move) as h.
         destruct h as [ abs | h].
         * exfalso.
@@ -4692,7 +4013,7 @@ destruct (active da) as [| id l] eqn:Hactive.
         * (* h and h' imply length (active da) == Nat.div2 (nG + nB) ===> contradiction. *)
           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 (forall (pt3 : location) (id3 : ident),
                      get_location (config id3) = pt3 ->
@@ -4783,7 +4104,7 @@ destruct (active da) as [| id l] eqn:Hactive.
               rewrite -> R2dec_bool_false_iff in heq.
               apply (h _ heq);auto.
               apply List.filter_In.
-              split;auto. }
+              split; auto. }
           rewrite <- H in h_not_div2_active.
           apply h_not_div2_active.
           rewrite all_white_active_moving;auto.
@@ -4799,9 +4120,8 @@ destruct (active da) as [| id l] eqn:Hactive.
           assumption.
         - exfalso.
           specialize (h_forall id_move).
-          apply h_forall;auto.
-          now symmetry. }
-      
+          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
@@ -4838,7 +4158,7 @@ destruct (active da) as [| id l] eqn:Hactive.
           tauto. }
         clear h.
         rewrite Forall_forall in h'.
-        
+
         specialize (h_cb_nb_wm id_move) as h.
         destruct h as [ abs | h].
         * exfalso.
@@ -4849,7 +4169,7 @@ destruct (active da) as [| id l] eqn:Hactive.
         * (* h and h' imply length (active da) == Nat.div2 (nG + nB) ===> contradiction. *)
           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 (forall (pt3 : location) (id3 : ident),
                      get_location (config id3) = pt3 ->
@@ -4897,13 +4217,6 @@ destruct (active da) as [| id l] eqn:Hactive.
               apply Decidable.dec_and.
               - red.
                 apply ListDec.In_decidable;try typeclasses eauto.
-                Lemma ident_eq_decidable: ListDec.decidable_eq ident.
-                Proof using.
-                  red.
-                  intros.
-                  red.
-                  destruct (names_eq_dec x y);auto.
-                Qed.
                 apply ident_eq_decidable.
               - apply get_location_dec. }
             intros abs.
@@ -4984,294 +4297,16 @@ destruct (active da) as [| id l] eqn:Hactive.
              ++ assumption.
   }
 Qed.
-          
+
 
 
 Lemma get_light_decb_spec id col: get_light (config id) = col <-> get_light_decb config col id = true.
-Proof.
+Proof using .
   unfold get_light_decb.
   destruct_match.
   - split;auto.
   - split;intro; try contradiction; try discriminate.
 Qed.
-(*
-Lemma color_bivalent_exists_symmetric: forall id,
-  exists id', get_location (config id') =/= get_location (config id)
-              /\ get_light (config id') == get_light (config id).
-Proof.
-  intros id. 
-  rewrite color_bivalent_iff in Hcolor.
-  destruct Hcolor as [pt1 [pt2 h_pt1pt2]].
-  red in h_pt1pt2.
-  unfold bivalent_on in h_pt1pt2.
-  destruct  h_pt1pt2 as [[h_neq_pt1_pt2 [h_biv1 h_biv2]] h_colbiv].
-  destruct (h_biv1 id).
-  - destruct (is_white_b config id) eqn:heq.
-    + assert (count_if (fun id => get_light_decb config true id
-                                  && R2dec_bool (get_location (config id)) pt1) >= 1) as h_id1.
-      { assert (InA equiv id names) as h_id_in.
-        { cbn -[names].
-          apply InA_Leibniz, In_names. }
-        
-        
-        destruct (PermutationA_split _ h_id_in) as [names' h_permut].
-        unfold count_if.
-        rewrite h_permut.
-        cbn -[get_location].
-        changeR2.
-        rewrite H.
-        rewrite R2dec_bool_refl.
-        unfold is_white_b in heq.
-        changeR2.
-        setoid_rewrite get_light_decb_spec in heq.
-        rewrite heq.
-        cbn.
-        lia. }
-(*
-      assert (count_if (fun id => get_light_decb config true id
-                               && R2dec_bool (get_location (config id)) pt2) >= 1) as h_id2.
-      { destruct (h_colbiv true) as [k [h h']].
-        rewrite h'.
-        rewrite <- h.
-        assumption. }
-
-      
-      rewrite H in *.
-      assert (exists id_sym,
-        List.In id_sym (List.filter (fun id => get_light_decb config true id
-                                               && R2dec_bool (get_location (config id)) pt2) names)) as h_sym.
-      { unfold count_if in h_id2.
-        match type of h_id2 with
-          length ?x >= _ => destruct x eqn:heq2
-        end.
-        - cbn in h_id2;inversion h_id2.
-        - match type of h_id2 with
-            length ?x >= _ => assert (InA equiv i x) as h_id_in
-          end.
-          { cbn -[names].
-            apply InA_Leibniz.
-            now constructor. }
-          exists i.
-          rewrite <- heq2 in h_id_in.
-          apply InA_Leibniz.
-          cbn -[names get_location] in h_id_in.
-          now constructor. }
-
-      destruct h_sym as [id_sym h_sym].
-      exists id_sym.
-      rewrite List.filter_In in h_sym.
-      destruct h_sym as [h_sym1 h_sym2].
-      apply andb_prop in h_sym2.
-      destruct h_sym2 as [h_sym2 h_sym3].
-      rewrite R2dec_bool_true_iff in h_sym3.
-      change eq with (@equiv _ bool_Setoid) in h_sym2.
-      split.
-      * rewrite h_sym3.
-        now symmetry.
-      * apply get_light_decb_spec in h_sym2.
-        symmetry.
-        rewrite h_sym2.
-        assumption.
-    +
-
-
-  assert (exists idblack2, get_location (config idblack2) =/= get_location (config idblack)
-                        /\ is_stationary config da idblack2).
-  { destruct (color_bivalent_exists_symmetic idblack).
-    exists x.
-    destruct H0.
-    split;auto.
-    apply black_dont_move;auto.
-    rewrite H1.
-    apply h_idblack.
-
-
-  destruct h_ex_moving as [id_move h_moving].
-  assert (forall x : ident,
-    {(fun id => is_stationary config da id /\ get_location (config id) =/= get_location (config idblack)) x}
-    + {~ (fun id => is_stationary config da id /\ get_location (config id) =/= get_location (config idblack)) x}) as h_dec.
-  { admit. }
-  edestruct (Exists_dec (fun id => is_stationary config da id
-                                /\ get_location (config id) =/= get_location (config idblack)) h_dec names).
-  * right.
-    red.
-    apply Exists_exists in e.
-    destruct e as [idothernotmoving [ h_In [h_nomove h_diff]]].
-    exists  id_move,idothernotmoving, idblack.
-    repeat split;auto.
-    symmetry ;auto.
-  * clear h_dec.
-    left.
-    red.
-    rewrite <- Forall_Exists_neg in n0.
-    rewrite Forall_forall in n0.
-    setoid_rewrite not_and in n0 ; auto with color_dec.
-    unfold is_stationary in n0.
-    
-    setoid_rewrite Decidable.not_not in n0.
-    rewrite Classical_Prop.NNPP in n0.
-
-
-    rewrite 
-
-    setoid_rewrite Decidable.not_not.
-    rewrite e 
-    exists idblack
-
-    exfalso.
-    apply n0.
-    apply Exists_exists.
-    exists idblack.
-    repeat split;auto.
-    ++ apply In_names.
-    ++ 
-  
-
-
-  Exists_dec
-  Exists_exists
-       
-
-unfold cb_nb_precondition_wholecolmove, cb_nb_precondition_somestay.
-
-(* assert (forall x : ident, get_light (config x) == false \/ ~ get_light (config x) == false). *)
-(* { intros x. cbn. destruct (get_light (config x)); intuition. } *)
-
-rewrite <- Exists_Forall_neg,Exists_exists in not_all_blacks;try discharge_dec.
-light_simp.
-destruct not_all_blacks as [id_active_white [h1_idw h2_idw]].
-(* At least one robot is moving. *)
-assert (List.In id_active_white (moving gatherR2 da config)).
-{ apply moving_iff.
-  split;auto. }
-rewrite not_and_3 in h_cb_b_allw;intros;try discharge_dec.
-do 2 rewrite <- Exists_Forall_neg in h_cb_b_allw;intros;try discharge_dec.
-repeat light_simp.
-Exists_impl
-setoid_rewrite not_true_iff_false in h_cb_b_allw.
-
-destruct (List.existsb (negb (mem equiv_dec id (moving gatherR2 da config))) )
-
-destruct (List.existsb
-            (fun id => andb (negb (mem equiv_dec id (moving gatherR2 da config)))
-                            (if equiv_dec (get_location (config id)) loc_g1 then true else false)
-            ) names) eqn:Heq.
-+ rewrite existsb_exists in Heq.
-  setoid_rewrite  andb_true_iff in Heq.
-  destruct Heq as [ x [ hIn [ hmem hloc]]].
-  destruct (List.existsb
-              (fun id => andb (negb (mem equiv_dec id (moving gatherR2 da config)))
-                           (if equiv_dec (get_location (config id)) loc_others then true else false)
-              ) names) eqn:Heq.
-  - right.
-    rewrite existsb_exists in Heq.
-    setoid_rewrite  andb_true_iff in Heq.
-    destruct Heq as [ y [ hIn' [ hmem' hloc' ]]].
-    red.
-    split.
-    { now exists id_white. }
-    exists x, y.
-    repeat split.
-    ** revert hloc hloc'.
-       repeat destruct_match; intuition.
-       rewrite H0,H1.
-       symmetry.
-       apply loc_g1_diff_others.
-    ** rewrite negb_true_iff in *.
-       apply mem_false_iff in hmem.
-       now rewrite <- InA_Leibniz.
-    ** rewrite negb_true_iff in *.
-       apply mem_false_iff in hmem'.
-       now rewrite <- InA_Leibniz.
-  -  (* h_cb_b_allw says that the case where *exactly* a whole column moves is not possible *)
-    (* repeat light_simp. *)
-    rewrite not_and_3 in h_cb_b_allw;intros;try discharge_dec.
-    do 2 rewrite <- Exists_Forall_neg in h_cb_b_allw;intros;try discharge_dec.
-    destruct h_cb_b_allw as [h | [h | h]]; try discharge_dec; repeat light_simp.
-    ** 
-    match goal with
-      H: existsb _ _ = false |- _ => rewrite <- negb_true_iff in H
-    end.
-    rewrite forallb_existsb in Heq.
-    rewrite forallb_forall in Heq.
-    setoid_rewrite negb_andb in Heq.
-    setoid_rewrite negb_involutive in Heq.
-    setoid_rewrite orb_comm in Heq.
-    setoid_rewrite <- implb_orb in Heq.
-    setoid_rewrite implb_true_iff in Heq.
-    left.
-    red.
-    exists g2.
-    split.
-    { admit. }
-    { exists id_white.
-      split;auto.
-      - symmetry.
-        apply g2_spec.
-      - 
-       }
-    exists x, g2.
-    repeat split;auto.
-    ++ destruct (get_location (config x) =?= loc_g1);try discriminate.
-       rewrite e.
-       apply g2_spec.
-    ++ enough (~ InA eq x (moving gatherR2 da config)).
-       { now rewrite <- InA_Leibniz. }
-       rewrite <- mem_false_iff.
-       apply hmem.
-    ++ apply Heq.
-    
-    setoid_rewrite negb_andb in Heq.
-    setoid_rewrite negb_involutive in Heq.
-    setoid_rewrite orb_true_iff in Heq.
-    light_simp.
-    rewrite existsb_exists in Heq.
-    
-
-    ** right. (* blacl on both sides. *)
-       admit.
-    **
-      rewrite (Exists_compat _ ) in h.
-      setoid_rewrite not_true_iff_false in h.
-
-      
-rewrite <- Exists_Forall_neg,Exists_exists in h;auto.
-       2:{ intros. cbn. destruct (bool_dec (get_light (config x0)) true);auto. }
-       admit.
-    ** apply Decidable.not_and in h.
-       2:{ apply Nat.eq_decidable. }
-       destruct h as [h|h].
-       ++ admit.
-       ++ rewrite <- Exists_Forall_neg,Exists_exists in h;auto.
-          2:{ intros x0.
-              destruct ((get_location (config x0)) =?= (get_location (config (hd (Good g1) (active da)))));auto. }
-          destruct h as [id_active_not_on_g1 [hactive hnot_on_g1]].
-          
-
-
-       
-    2: apply Decidable.not_and in h.
-    3:{ apply Nat.eq_decidable. }
-    2:destruct h as [h|h].
-    
-        
-        
-
-
-    rewrite <- Exists_Forall_neg,Exists_exists in h;auto.
-
-    
-
-
-    admit.
-+ left. (* same argument for other column *)
-  admit.
-*)
-Admitted. *)
-(*   (* Half the robots are active *)
-  /\ length (active da) = Nat.div2 (nG + nB)
-  (* All active robots are on a single tower *)
-  /\ Forall (fun id => get_location (config id) == get_location (config (hd (Good g1) (active da)))) (active da). *)
 
 Theorem color_bivalent_round_lt_config :
   changing gatherR2 da config <> nil ->
@@ -5462,7 +4497,7 @@ Qed.
 Corollary not_color_bivalent_moving_target : forall id, List.In id (moving gatherR2 da config) ->
   get_location (round gatherR2 da config id)
   == find_other_loc (fst (!!! (config, config id))) (get_location (config id)).
-Proof.
+Proof using Hssync Hbivalent Hcolor.
 intros id Hid.
 rewrite not_color_bivalent_target.
 + rewrite moving_spec in Hid.
@@ -5605,7 +4640,7 @@ Qed.
 Lemma not_color_bivalent_next :
   moving gatherR2 da config <> nil ->
   exists pt, MajTower_at pt (round gatherR2 da config).
-Proof.
+Proof using Hssync Hbivalent Hcolor.
 intro Hmove.
 assert (Hevolve := not_color_bivalent_wither_and_grow).
 destruct (moving gatherR2 da config) as [| id l] eqn:Hmoving; try tauto; [].
@@ -5695,7 +4730,7 @@ Hypothesis Hbivalent : ~ bivalent config.
 
 Corollary round_simplify_Lights : forall id,
   get_light (round gatherR2 da config id) == get_light (config id).
-Proof.
+Proof using Hssync Hbivalent.
 intro id.
 assert (Hrew := round_simplify_non_bivalent).
 eapply get_light_compat in Hrew; eauto; []. rewrite Hrew.
@@ -6005,7 +5040,6 @@ cut ((!! config)[target (!! config)] < (!! (round gatherR2 da config))[target (!
 Qed.
 
 Opaque obs_from_config.
-(* Opaque R2_Setoid. *)
 
 Lemma solve_measure_dirty :
   moving gatherR2 da config <> nil ->
@@ -6042,8 +5076,6 @@ unfold f in Hext.
 rewrite (filter_extensionality_compat _ _ Hext). clear Hext.
 pose (f_target := fun x => if equiv_dec x (target (!! config)) then true else false).
 pose (f_out_target := fun x => if InA_dec equiv_dec x (SECT (!! config)) then negb (f_target x) else false).
-(* assert (Proper (equiv ==> eq) f_target).
-{ intros ? ? Heq. simpl in Heq. subst. unfold f_target. R2dec_full. } *)
 assert (Hext : forall x, f (!! config) x = f_target x || f_out_target x).
 { intro pt. unfold f, f_out_target, f_target. simpl. changeR2. repeat destruct_match; reflexivity. }
 unfold f in Hext. setoid_rewrite (filter_extensionality_compat _ _ Hext). clear Hext f.
@@ -6156,8 +5188,6 @@ destruct (support (max (!! config))) as [| pt [| pt' l']] eqn:Hmaj.
         + repeat constructor.
           - intro Habs. inversion Habs. now elim Hdiff. now inversion H.
           - intro Habs. now inversion Habs.
-        (* NoDupA_Leibniz had a useless hyp in coq stdlib until april 2020. *)
-        (* + rewrite <- NoDupA_Leibniz. change eq with (@equiv location _). apply support_NoDupA. *)
         + now setoid_rewrite <- (bivalent_size (origin, witness) Hbivalent').
         + intros pt Hpt. inversion_clear Hpt.
           - subst. rewrite <- InA_Leibniz. change eq with (@equiv location _). rewrite support_spec.
@@ -6748,7 +5778,7 @@ destruct (support (max (!! (round gatherR2 da config)))) as [| pt1 [| pt2 l]] eq
                       left.
                       reflexivity. }
             --- (* (ptx :: pty :: ptz :: nil) = (middle pt1 pt2 :: pt1 :: pt2 :: nil)
-                   contradiction with calssify_triangle = equilateral *)
+                   contradiction with classify_triangle = equilateral *)
               assert (PermutationA equiv (ptx :: pty :: ptz :: nil) (middle pt1 pt2 :: pt1 :: pt2 :: nil)).
               { apply inclA_skip in Hincl;autoclass.
                 - symmetry.
@@ -7114,9 +6144,8 @@ destruct (support (max (!! (round gatherR2 da config)))) as [| pt1 [| pt2 l]] eq
                   - rewrite <- Hsec'. unfold on_SEC. intro. rewrite (filter_InA _). intuition.
                   - rewrite <- size_spec. rewrite Hlen. cbn. lia. }
                 rewrite <- Hsec' in Hperm'.
-                (* Triangle equilatéral: comme qqchose bouge et que on est encore avec 3
-                   colonne après, une colonne s'est déplacée vers le barycentre, contradiction:
-                   le barycentre ne peut pas être sur le SEC. *)
+                (* Equilateral triangle: since one robot moves and there are still 3 columns afterwards,
+                   a column moved to the barycenter, contradiction as the barycenter cannot be on the SEC. *)
                 assert (Hnodup : NoDupA equiv (ptx :: pty :: ptz :: nil)).
                 { rewrite <- Hsec. apply on_SEC_NoDupA, support_NoDupA. }
                 assert (Hex : exists pta ptb ptc,
@@ -7968,7 +6997,7 @@ Definition unfair_gathering r d config :=
    robot can move, then some robot moves *)
 
 Definition sim_da_with_all_activated da : similarity_da.
-Proof.
+Proof using .
 exists (da_with_all_activated da).
 apply (proj2_sig da).
 Defined.
@@ -8027,4 +7056,4 @@ End GatheringInR2.
 
 (* this is ignored when coq -vos is used. This will fail when coqtop
    if relying on .vos. But it will succeed when using .vo *)
-(* Print Assumptions Gathering_in_R2.  *)
+(* Print Assumptions Gathering_in_R2. *)
diff --git a/Spaces/R2.v b/Spaces/R2.v
index ae12cac1ec91672c1bdf083f5be7561cda71bd46..5ba7fcb584327ae0dcf658dbf98e2e2bd803d5e1 100644
--- a/Spaces/R2.v
+++ b/Spaces/R2.v
@@ -1714,7 +1714,7 @@ Proof using .
 Qed.
 
 Lemma middle_diff: forall ptx pty,
-  ptx <> pty -> ~InA equiv (middle ptx pty) (ptx :: pty :: nil).
+  ptx =/= pty -> ~InA equiv (middle ptx pty) (ptx :: pty :: nil).
 Proof using .
 intros ptx pty Hdiff Hin.
 inversion_clear Hin; subst.
diff --git a/Util/Preliminary.v b/Util/Preliminary.v
index 82066e62d7c13399753c690b0fb7274ac418127c..bfa4c8ca888911e048b433dad98501241e429263 100644
--- a/Util/Preliminary.v
+++ b/Util/Preliminary.v
@@ -30,7 +30,7 @@ Ltac autoclass := eauto with typeclass_instances.
 Ltac inv H := inversion H; subst; clear H.
 Hint Extern 1 (equiv ?x ?x) => reflexivity : core.
 Hint Extern 2 (equiv ?y ?x) => now symmetry : core.
-
+Hint Unfold complement : core.
 
 (** **  Tactics  **)