proposition: Lemma hauteur_isocele_mediane : forall A B C I : PO, B <> C -> orthogonal (vec B C) (vec I A) -> isocele A B C -> alignes B C I -> I = milieu B C.
proof: Proof. intros A B C I H0 H1 H2 H3; try assumption. soit_projete B C A H. apply mediatrice_projete_milieu with A; auto. rewrite <- H4. apply unicite_projete_orthogonal with (3 := H1); auto. Qed.