proposition: Lemma map_arc (aT rT : eqType) (f : aT -> rT) (s : seq aT) (x y : aT) : injective f -> [seq f z | z <- arc s x y] = arc (map f s) (f x) (f y).
proof: Proof. by move=> inj_f; rewrite /arc -map_rot !index_map // map_take. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)