proposition: Lemma mediatrice_droite : forall A B I J K : PO, A <> B :>PO -> I = milieu A B :>PO -> mediatrice A B J -> mediatrice A B K -> alignes I J K.
proof: Proof. intros. discrimine I J. discrimine J K. discrimine I K. lapply (milieu_mediatrice (A:=A) (B:=B) (M:=I)); auto; intros. lapply (mediatrice_orthogonale_segment (A:=A) (B:=B) (M:=I) (N:=J)); auto; intros. lapply (mediatrice_orthogonale_segment (A:=A) (B:=B) (M:=I) (N:=K)); auto; intros. elim (orthogonal_paralleles (A:=I) (B:=B) (C:=J) (E:=I) (F:=K)); auto; intros. apply colineaire_alignes with x; auto. lapply (milieu_distinct2 (A:=A) (B:=B)); auto. rewrite <- H0; auto. lapply (orthogonal_segment_milieu (A:=A) (B:=B) (C:=I) (D:=J) (I:=I)); auto; intros. elim H9; auto with geo; intros. apply ortho_sym. lapply (orthogonal_segment_milieu (A:=A) (B:=B) (C:=I) (D:=K) (I:=I)); auto; intros. elim H9; auto with geo; intros. Qed.