proposition: Lemma milieu_centrecirconscrit_orthogonal_segment : forall A B C A' O : PO, A' = milieu B C -> circonscrit O A B C -> orthogonal (vec O A') (vec B C).
proof: Proof. unfold circonscrit, isocele in |- *; intros. elim H0; intros H1 H2; try clear H0; try exact H2. discrimine O A'. apply ortho_sym. replace (vec A' A') with zero; [ idtac | Ringvec ]. auto with geo. discrimine B C. replace (vec C C) with zero; [ auto with geo | Ringvec ]. apply mediatrice_orthogonale_segment; auto. unfold mediatrice in |- *. rewrite <- H1; auto. apply milieu_mediatrice; auto. Qed.