proposition: Lemma mediatrice_projete_milieu : forall A B M H : PO, A <> B :>PO -> H = projete_orthogonal A B M :>PO -> mediatrice A B M -> H = milieu A B :>PO.
proof: Proof. intros. generalize (def_projete_orthogonal2 (A:=A) (B:=B) (C:=M) (H:=H)); intros. elim H3; [ intros; clear H3 | auto | auto ]. apply alignes_mediatrice_milieu; auto. red in |- *. apply mediatrice_projete_orthogonal with M; auto. Qed.