proposition: Lemma paralleles_alignes2 : forall A B C D E F : PO, A <> B :>PO -> C <> D :>PO -> vec E F = vec A B :>PP -> paralleles (droite A B) (droite C D) -> alignes C D E -> alignes F C E.
proof: Proof. intros A B C D E F H H0 H1 H2 H3; try assumption. elim (paralleles_vecteur (A:=C) (B:=D) (C:=A) (D:=B)); intros; auto with geo. halignes H3 x0. rewrite H4 in H5. discrimine F C. cut (1 + x0 * x <> 0); intros. apply colineaire_alignes with (/ (1 + x0 * x)). VReplace (vec F C) (add_PP (vec F E) (mult_PP (-1) (vec C E))). VReplace (vec F E) (mult_PP (-1) (vec E F)). rewrite H1; rewrite H5. Fieldvec (1 + x0 * x). red in |- *; intros; apply H6. apply vecteur_nul_conf. VReplace (vec F C) (add_PP (mult_PP (-1) (vec E F)) (mult_PP (-1) (vec C E))). rewrite H1; rewrite H5. VReplace (add_PP (mult_PP (-1) (vec A B)) (mult_PP (-1) (mult_PP x0 (mult_PP x (vec A B))))) (mult_PP (-1) (mult_PP (1 + x0 * x) (vec A B))). rewrite H7; Ringvec. Qed.