proposition: Lemma alignes_paralleles_confondus : forall A B C J : PO, triangle A B C -> alignes A C J -> paralleles (droite B C) (droite B J) -> J = C :>PO.
proof: Proof. intros. cut (triangle B C A); auto with geo; intros. deroule_triangle B C A. apply (concours_unique (A:=B) (B:=A) (A1:=C) (B1:=C) (I:=J) (J:=C)); auto with geo. cut (B <> J); intros. elim paralleles_vecteur with (A := B) (B := J) (C := B) (D := C); [ intros k0 H8 | auto | auto | auto with geo ]. apply colineaire_alignes with k0; auto. cut (triangle A C B); auto with geo; intros. deroule_triangle A C B. red in |- *; intros; apply H8. rewrite H12; auto. Qed.