proposition: Lemma equation_droite_parallele : 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) -> paralleles (droite A B) (droite C D) -> b * (x + - x0) + - (a * (y + - y0)) = 0.
proof: Proof. intros. apply vec_directeur_calcul with (1 := H) (2 := H0); auto with geo. Qed.