fact: Definition smoothen (s : seq (annotated_point * annotated_point)) : seq curve_element := match s with | (a, b) :: tl => straight a b :: smoothen_aux tl | nil => nil end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL