proposition: Lemma vec_directeur_calcul : forall (A B C D : PO) (x y x0 y0 a b : R), A <> B -> C <> D -> x = abscisse D -> y = ordonnee D -> x0 = abscisse C -> y0 = ordonnee C -> a = absvec (vec A B) -> b = ordvec (vec A B) -> vec_directeur (vec A B) (droite C D) -> b * (x + - x0) + - (a * (y + - y0)) = 0.
proof: Proof. intros A B C D x y x0 y0 a b H H0 H1 H2 H3 H4 H5 H6 H7; try assumption. cut (vec C D = add_PP (mult_PP (x + - x0) (vec O I)) (mult_PP (y + - y0) (vec O J))); intros. 2: apply composantes_vecAB; eauto with geo. cut (vec A B = add_PP (mult_PP a (vec O I)) (mult_PP b (vec O J))); [ intros | auto with geo ]. RReplace 0 (-0). rewrite <- (vec_directeur_def (A:=A) (B:=B) (C:=C) (D:=D)); auto. rewrite (determinant_def (A:=A) (B:=B) (C:=C) (D:=D) (x:=a) (y:=b) (x':= x + - x0) (y':=y + - y0)); auto. ring. Qed.