proposition: Lemma orthogonal_colineaires : forall A B C D E F : PO, A <> B :>PO -> C <> D :>PO -> orthogonal (vec A B) (vec C D) -> orthogonal (vec A B) (vec E F) -> ex (fun k : R => vec E F = mult_PP k (vec C D) :>PP).
proof: Proof. intros. elim existence_representant_vecteur with (A := A) (B := C) (C := D); intros C1 H5; try clear existence_representant_vecteur; try exact H5. rewrite <- H5. elim orthogonal_paralleles with (A := A) (B := B) (C := C1) (E := E) (F := F); [ intros k H3; try clear orthogonal_paralleles; try exact H3 | auto | auto | auto | auto with geo ]. exists k; auto. apply distinct_egalite_vecteur with (2 := H5); auto. rewrite H5; auto with geo. Qed.