proposition: Lemma vert_projr (p q r : Plane R) : p.1 != q.1 -> (det p q r == 0) = (r.2 == q.2 + (r.1 - q.1) / (q.1 - p.1) * (q.2 - p.2)).
proof: Proof. case: p q r=> [p1 p2][q1 q2][r1 r2] /=; rewrite develop_det /= => e_cnd. apply/idP/eqP; last first. move=> -> /=; rewrite !mulrDl -(opprB q1 p1) !mulrN (mulrAC _ _ (q1 - p1)). rewrite mulfVK; last by rewrite subr_eq0 eq_sym. rewrite (mulrAC _ _ (q1 - p1)). rewrite mulfVK; last by rewrite subr_eq0 eq_sym. apply/eqP; ring. rewrite !(addrAC _ (- (r2 * (p1 - q1)))) subr_eq0 eq_sym => /eqP r2Mdf. have dn0 : (p1 - q1) != 0 by rewrite subr_eq0. apply: (mulIf dn0); rewrite r2Mdf mulrDl (mulrAC _ _ (p1 - q1)) -(opprB p1 q1). rewrite invrN !(mulrN, mulNr). rewrite mulfVK //; ring. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection