proposition: Lemma permutation_nodes : Permutation nodes (map tot_map_name nodes).
proof: Proof. Proof using name_map_bijective. apply: NoDup_Permutation; last split. - exact: no_dup_nodes. - apply nodup_to_map_name. exact: no_dup_nodes. - move => H_in. set x' := tot_map_name_inv x. have H_in' := all_names_nodes x'. apply in_split in H_in'. move: H_in' => [ns1 [ns2 H_eq]]. rewrite H_eq map_app /= /x'. apply in_or_app. right; left. by rewrite tot_map_name_inverse_inv. - move => H_in. exact: all_names_nodes. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)