proposition: Lemma mediatrices_triangle_concours : forall A B C I J K L : PO, triangle A B C -> I = milieu A B :>PO -> J = milieu B C :>PO -> I <> K :>PO -> J <> L :>PO -> mediatrice A B K -> mediatrice B C L -> concours (droite I K) (droite J L).
proof: Proof. intros. deroule_triangle A B C. lapply (position_relative_droites_coplanaires (A:=I) (B:=K) (C:=J) (D:=L)); auto with geo; intros. elim H10; auto with geo; intros. absurd (paralleles (droite J L) (droite I K)); auto with geo. cut (double_AV (cons_AV (vec I K) (vec J L)) = double_AV (cons_AV (vec B A) (vec B C))); intros. apply angle_non_paralleles; auto. rewrite H12. red in |- *; intros. apply H6; auto with geo. apply angles_droites_orthogonales; auto. cut (orthogonal (vec I K) (vec A B)); intros; auto with geo. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. apply ortho_sym; auto. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. Qed.