fact: Fixpoint seq_to_intervals_aux [A : Type] (a : A) (s : seq A) := match s with | nil => nil | b :: tl => (a, b) :: seq_to_intervals_aux b tl end.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection