fact: Definition path_reverse (s : seq (annotated_point * annotated_point)) := List.map (fun p => (snd p, fst p)) (List.rev_append s nil).
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL