proposition: Lemma isocele_mediane_bissectrice : forall A B C I : PO, A <> I -> B <> C -> I = milieu B C -> isocele A B C -> cons_AV (vec A B) (vec A I) = cons_AV (vec A I) (vec A C).
proof: Proof. intros. apply mediatrice_milieu_angles; auto. Qed.