proposition: Lemma seq_to_intervals_rcons [A : Type](e1 e2 : A) l : seq_to_intervals (rcons (rcons l e2) e1) = rcons (seq_to_intervals (rcons l e2)) (e2, e1).
proof: Proof. by elim: l => [// | e3 [// | e4 l] /= Ih] //; rewrite Ih. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection