proposition: Theorem unicite_circonscrit_triangle : forall A B C O O1 : PO, triangle A B C -> circonscrit O A B C -> circonscrit O1 A B C -> O = O1.
proof: Proof. intros. deroule_triangle A B C. soit_mediatrice A B M K. soit_mediatrice B C J L. lapply (mediatrices_triangle_concours (A:=A) (B:=B) (C:=C) (I:=M) (J:=J) (K:=K) (L:=L)); auto; intros. cut (M <> J); intros. generalize H1; unfold circonscrit in |- *; intros. generalize H0; unfold circonscrit in |- *; intros. lapply (circonscrit_isocele (O:=O) (A:=A) (B:=B) (C:=C)); auto; intros. lapply (circonscrit_isocele (O:=O1) (A:=A) (B:=B) (C:=C)); auto; intros. elim H22; (clear H22; intros). elim H23; (clear H23; intros). lapply (milieu_mediatrice (A:=A) (B:=B) (M:=M)); auto; intros. lapply (milieu_mediatrice (A:=B) (B:=C) (M:=J)); auto; intros. lapply (mediatrice_droite (A:=A) (B:=B) (I:=M) (J:=K) (K:=O)); auto; intros. lapply (mediatrice_droite (A:=B) (B:=C) (I:=J) (J:=L) (K:=O)); auto; intros. lapply (mediatrice_droite (A:=A) (B:=B) (I:=M) (J:=K) (K:=O1)); auto; intros. lapply (mediatrice_droite (A:=B) (B:=C) (I:=J) (J:=L) (K:=O1)); auto; intros. cut (double_AV (cons_AV (vec M K) (vec J L)) = double_AV (cons_AV (vec B A) (vec B C))). intros H101. elim (classic (alignes J M L)); intros. apply (concours_unique (A:=M) (B:=J) (A1:=K) (B1:=M) (I:=O) (J:=O1)). red in |- *; intros; apply H2. cut (double_AV (cons_AV (vec M K) (vec M J)) = double_AV (cons_AV (vec B A) (vec B C))); intros. apply permute_alignes; auto. apply alignes_angle; auto. rewrite <- H36. apply angle_alignes; auto. rewrite <- H101. halignes H34 x. absurd (J = M); auto. cut (vec J L = mult_PP (- x) (vec M J)); intros. cut (vec M K = mult_PP 1 (vec M K)); intros. apply angles_et_colinearite with (5 := H38) (6 := H37); auto. Ringvec. rewrite H36. Ringvec. auto. apply H30; auto. discrimine O M. discrimine O J. apply alignes_ordre_cycle; auto. apply alignes_ordre_cycle; auto. apply alignes_trans with (B := L); auto with geo. apply H32; auto. discrimine O1 M. discrimine O1 J. apply alignes_ordre_cycle; auto. apply alignes_ordre_cycle; auto. apply alignes_trans with (B := L); auto with geo. apply (concours_unique (A:=J) (B:=M) (A1:=L) (B1:=K) (I:=O) (J:=O1)); auto. red in |- *; intros; apply H34. apply alignes_ordre_permute; auto. discrimine O M. discrimine O K. apply alignes_ordre_cycle; auto with geo. discrimine O1 M. discrimine O1 K. apply alignes_ordre_cycle; auto with geo. apply angles_droites_orthogonales; auto. cut (orthogonal (vec M K) (vec A B)); intros; auto with geo. apply mediatrice_orthogonale_segment; auto. apply ortho_sym; auto. apply mediatrice_orthogonale_segment; auto. apply deux_milieux_distincts with (2 := H11) (3 := H18); auto. Qed.