proposition: Lemma vec_normal_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_normal (vec A B) (droite C D) -> a * (x + - x0) + b * (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. elim existence_representant_vecteur with (A := O) (B := A) (C := B); [ intros M H10 ]. elim existence_representant_vecteur with (A := O) (B := C) (C := D); [ intros N H20 ]. 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 ]. replace 0 with (scalaire (vec A B) (vec C D)); auto with geo. rewrite <- H10; rewrite <- H20. rewrite (scalaire_coordonnees (O:=O) (I:=I) (J:=J) (M:=M) (N:=N) (x:=a) (y:=b) (x':=x + - x0) (y':=y + - y0)); auto with geo. rewrite H10; auto. rewrite H20; auto. Qed.