proposition: Lemma centre_circonscrit_rectangle_milieu : forall A B C C' O : PO, triangle A B C -> C' = milieu A B -> circonscrit O A B C -> orthogonal (vec C A) (vec C B) -> O = C'.
proof: Proof. intros. deroule_triangle A B C. deroule_circonscrit A B C O. rewrite H0. cut (cons_AV (vec O A) (vec O B) = image_angle pi); intros. cut (alignes O A B); intros. apply alignes_mediatrice_milieu; auto with geo. unfold mediatrice in |- *. elim H1; auto. apply alignes_angle; auto. unfold double_AV in |- *. rewrite H10. repeat rewrite <- add_mes_compatible. replace (pi + pi) with deuxpi; auto. rewrite pi_plus_pi; auto. rewrite <- (angle_inscrit (O:=O) (A:=C) (B:=A) (C:=B)); auto. apply orthogonal_angles; auto. apply circonscrit_permute; auto. Qed.