proposition: Lemma bezier_on_vertical_line (a b c : Plane R) (v : vert_edge) : a.1 < b.1 < c.1 -> {u | u \in `]0, 1[ & (bezier (f3pt a b c) 2 u).1 = b.1}.
proof: Proof. move=> abc. set bezierx := \sum_(i < 3) ((f3pt a b c) i).1 *: bernp 0 1 2 i - b.1%:P. have bezierxq t : (bezier (f3pt a b c) 2 t).1 = (bezierx + b.1%:P).[t]. rewrite bezier_bernstein2 /bezierx. rewrite addrNK !big_ord_recr /= !big_ord0 /= !add0r. have expandscale (x y : R) : x *: (y : R^o) = x * y by []. rewrite 3![in RHS] hornerE !hornerZ !expandscale. Fail ring. by rewrite (mulrC a.1) (mulrC b.1) (mulrC c.1). have bz0 : bezier (f3pt a b c) 2 0 = a. by rewrite !bezier_step_conv /= !conv0. have bz1 : bezier (f3pt a b c) 2 1 = c. by rewrite !bezier_step_conv /= !conv1. have : bezierx.[0] < 0. move: (bezierxq 0); rewrite bz0 hornerE [X in _ + X]hornerE. move=> /eqP; rewrite -subr_eq=> /eqP <-. by rewrite subr_lt0; case/andP: abc. have : 0 < bezierx.[1]. move: (bezierxq 1); rewrite bz1 hornerE [X in _ + X]hornerE. move=> /eqP; rewrite -subr_eq=> /eqP <-. by rewrite subr_gt0; case/andP: abc. move=> /gtr0_sg sg1 /ltr0_sg sg0. have sgM : Num.sg bezierx.[0] * Num.sg bezierx.[1] = -1. by rewrite sg1 sg0 mulr1. have [u uint /rootP ur] := ivt_sign ler01 sgM. exists u=> //. by rewrite bezierxq hornerE ur add0r hornerE. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection