proposition: Lemma diff_vert_y (a b c c' : Plane R) : a.1 != b.1 -> c' = (c.1, a.2 + (c.1 - a.1) / (b.1 - a.1) * (b.2 - a.2)) -> (c.2 - c'.2 ) = det a b c / (b.1 - a.1).
proof: Proof. intros anb c'def. have dn0 : b.1 - (a.1 : R^o) != 0. by rewrite subr_eq0 eq_sym. rewrite c'def /= (mulrAC _ _ (b.2 - a.2)) opprD addrA. apply: (mulIf dn0); rewrite mulrBl !mulfVK //. rewrite det_scalar_productE /rotate /scalar_product /= mulrN. by rewrite mulrC; congr (_ - _); rewrite mulrC. Qed.
imports: mathcomp(all_ssreflect all_algebra all_real_closed reals) mathcomp.algebra_tactics(ring lra) casteljau convex counterclockwise intersection