proposition: Lemma orthogonal_diametre_cercle : forall A B C A' O D : PO, triangle A B C -> circonscrit O A B C -> O = milieu A A' -> orthogonal (vec D A) (vec D A') -> sont_cocycliques A B C D.
proof: Proof. intros. discrimine D A. discrimine D A'. generalize H0; unfold sont_cocycliques, circonscrit, isocele in |- *; intros. exists O. split; [ try assumption | idtac ]. elim H5; intros H6 H7; try clear H5; try exact H6. split; [ try assumption | idtac ]. apply milieu_distance; auto. cut (circonscrit O A A' D); intros. generalize H0; generalize H5. unfold sont_cocycliques, circonscrit, isocele in |- *; intros. exists O. split; [ try assumption | idtac ]. elim H7; intros H8 H9; try clear H7; try exact H9. elim H6; intros H7 H10; try clear H6; try exact H10. split; auto. cut (triangle D A A'); intros. elim existence_cercle_circonscrit with (A := A) (B := A') (C := D); [ intros I H7 | auto with geo ]. cut (I = O); intros. rewrite <- H6; auto with geo. generalize (centre_circonscrit_rectangle_milieu (A:=A) (B:=A') (C:=D)); intros H8; apply H8; auto with geo. unfold triangle in |- *. apply orthogonal_non_alignes; auto. Qed.