proposition: Lemma mediatrice_orthogonale_segment_milieu : forall A B M N : PO, A <> B :>PO -> M <> N :>PO -> M = milieu A B :>PO -> mediatrice A B N -> orthogonal (vec A B) (vec M N).
proof: Proof. intros A B M N H3 H0 H1 H2; try assumption. elim existence_projete_orthogonal with (A := A) (B := B) (C := N); [ intros H H4; try clear existence_projete_orthogonal; auto | auto ]. generalize (mediatrice_projete_milieu (A:=A) (B:=B) (M:=N) (H:=H)); intros H7. rewrite H1; rewrite <- H7; auto. generalize (def_projete_orthogonal2 (A:=A) (B:=B) (C:=N) (H:=H)); intros. elim H5; [ intros; auto | auto | auto ]. Qed.