proposition: Lemma height_bezier2 (a b c p : Plane R) t: a.1 < b.1 < c.1 -> det a b p = 0 -> p.1 = (bezier (f3pt a b c) 2 t).1 -> (bezier (f3pt a b c) 2 t).2 - p.2 = t ^ 2 * det a b c / (b.1 - a.1).
proof: Proof. move=> abcdq p1q palign. set c' := (c.1, a.2 + (c.1 - a.1) / (b.1 - a.1) * (b.2 - a.2)). have anb : a.1 != b.1 by lra. rewrite -[RHS]mulrA -(diff_vert_y anb erefl). move: p1q palign => /eqP. rewrite vert_projr; last by lra. move=> /eqP /[dup] palign -> projP. rewrite (mulrAC _ _ (b.2 - a.2)). have dba : b.1 - a.1 != 0 by lra. apply: (mulIf dba). rewrite mulrBl (mulrDl b.2) mulfVK // projP. rewrite (mulrBr (t ^ 2)) (mulrBl (b.1 - a.1)). have tmp1 : t ^ 2 * c'.2 * (b.1 - a.1) = t ^ 2 * (a.2 * ( b.1 - a.1) + (c.1 - a.1) * (b.2 - a.2)). rewrite -mulrA; congr (_ * _). by rewrite /= mulrDl (mulrAC _ _ (b.1 - a.1)) mulfVK. rewrite !bezier_step_conv /=. have tmp x (y : R^o) : x *: y = x * y by []. rewrite !tmp tmp1. ring. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection