Some tools useful to Even added here as well.

Core/Identifiers.v

@@ -116,10 +116,14 @@ unfold names in Heq. repeat rewrite ?map_app, map_map in Heq. apply eqlistA_app_
 + now do 2 rewrite map_length.
 Qed.
 
+Section Robots.
+
+Context (n m : nat) {ln lm : nat} {ltc_l_n : ln <c n} {ltc_l_m : lm <c m}.
+
 (** Given a number of correct and Byzantine robots, we can build canonical names.
     It is not declared as a global instance to avoid creating spurious settings. *)
-Definition Robots (n m : nat) : Names.
-Proof using .
+Definition Robots : Names.
+Proof using n m.
   refine {|
     nG := n;
     nB := m;
@@ -138,5 +142,37 @@ Proof using .
   + intros ? ?. apply enum_eq.
   + intros ? ?. apply enum_eq.
 Defined.
-
 Global Opaque G B.
+
+Notation G := (@G Robots).
+Notation B := (@B Robots).
+
+Lemma G_Robots : G = fin n.
+Proof using . reflexivity. Qed.
+
+Lemma B_Robots : B = fin m.
+Proof using . reflexivity. Qed.
+
+Lemma G_Robots_eq_iff : ∀ g1 g2 : G, g1 = g2 :> G <-> g1 = g2 :> fin n.
+Proof using . reflexivity. Qed.
+
+Lemma B_Robots_eq_iff : ∀ b1 b2 : B, b1 = b2 :> B <-> b1 = b2 :> fin m.
+Proof using . reflexivity. Qed.
+
+Definition good0 : G := fin0.
+
+Definition byz0 : B := fin0.
+
+Lemma all_good0 : ∀ g : G, n = 1 -> g = good0.
+Proof using . intros * H. rewrite G_Robots_eq_iff. apply all_fin0, H. Qed.
+
+Lemma all_good_eq : ∀ g1 g2 : G, n = 1 -> g1 = g2.
+Proof using ltc_l_n. intros * H. rewrite G_Robots_eq_iff. apply all_eq, H. Qed.
+
+Lemma all_byz0 : ∀ b : B, m = 1 -> b = byz0.
+Proof using . intros * H. rewrite B_Robots_eq_iff. apply all_fin0, H. Qed.
+
+Lemma all_byz_eq : ∀ b1 b2 : B, m = 1 -> b1 = b2.
+Proof using ltc_l_m. intros * H. rewrite B_Robots_eq_iff. apply all_eq, H. Qed.
+
+End Robots.

Spaces/Ring.v

@@ -538,6 +538,9 @@ Proof using .
   specialize (H v2). rewrite (asbfE v1), (asbfE v2) in H. apply H.
 Qed.
 
+Lemma transs : ∀ v : fin n, trans v v = fin0.
+Proof using . intros. rewrite transvE. apply asbfVf. Qed.
+
 Definition sym (v : fin n) : isomorphism Ring.
 Proof using .
   refine {|
@@ -575,4 +578,7 @@ Lemma move_along_sym : ∀ (v1 v2 : fin n) (d : direction),
   move_along (sym v1 v2) d = sym v1 (move_along v2 (swap_direction d)).
 Proof using . intros. rewrite symvE, (sybfE v1). apply move_along_symf. Qed.
 
+Lemma symm : ∀ v : fin n, sym v v = v.
+Proof using . intros. rewrite symvE. apply sybff. Qed.
+
 End Ring.

Util/Fin.v

@@ -1603,6 +1603,9 @@ Proof using .
   intros * f3. rewrite compE, 3 asbfVE, asbfE, addf_subf. apply subf_subf.
 Qed.
 
+Lemma asbfVf : ∀ f : fin u, (asbf f)⁻¹ f = fin0.
+Proof using . intros. rewrite asbfVE. apply subff. Qed.
+
 (*
  *
  *            The bijection on fin u whose section is sucf
@@ -1696,4 +1699,7 @@ Proof using . intros c f. rewrite sybfE, sybfVE. reflexivity. Qed.
 Lemma sybfK : ∀ c : fin u, sybf c ∘ sybf c == id.
 Proof using . intros c f. rewrite compE, sybfE. apply symfK. Qed.
 
+Lemma sybff : ∀ c : fin u, sybf c c = c.
+Proof using . intros. rewrite sybfE. apply symff. Qed.
+
 End mod2fin.