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