proposition: Lemma mediane_hauteur_isocele : forall A B C I : PO, I = milieu B C -> orthogonal (vec B C) (vec I A) -> isocele A B C.
proof: Proof. intros. apply mediatrice_isocele. discrimine B C. unfold mediatrice in |- *; auto with geo. apply orthogonale_segment_milieu_mediatrice with I; auto. Qed.