proposition: Lemma mediane_isocele_hauteur : forall A B C I : PO, I = milieu B C -> isocele A B C -> orthogonal (vec I A) (vec B C).
proof: Proof. intros. discrimine B C. VReplace (vec C C) zero. auto with geo. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. Qed.