proposition: Theorem reciproque_cocyclicite : forall A B C D : PO, triangle A B C -> triangle A B D -> double_AV (cons_AV (vec C A) (vec C B)) = double_AV (cons_AV (vec D A) (vec D B)) -> sont_cocycliques A B C D.
proof: Proof. unfold sont_cocycliques in |- *; intros. deroule_triangle A B C. deroule_triangle A B D. soit_circonscrit A B C O2. soit_circonscrit A B D O1. mesure C A C B. lapply (angle_inscrit2 (O:=O2) (A:=A) (B:=B) (C:=C)); auto; intros. lapply (angle_inscrit2 (O:=O1) (A:=A) (B:=B) (C:=D)); auto; intros. exists O2. split; [ try assumption | idtac ]. unfold circonscrit in |- *. split; [ try assumption | idtac ]. elim H10; auto. cut (double_AV (cons_AV (vec C A) (vec C B)) <> image_angle 0); [ intros H50 | idtac ]. cut (O2 = O1); intros. rewrite H21. elim H12; auto. soit_mediatrice A B M J. elim (circonscrit_mediatrice (O:=O2) (A:=A) (B:=B) (C:=C)); try assumption; intros H60 H61. elim H61; clear H61; intros H61 H62. elim (circonscrit_mediatrice (O:=O1) (A:=A) (B:=B) (C:=D)); try assumption; intros H70 H71. elim H71; clear H71; intros H71 H72. lapply (mediatrice_droite (A:=A) (B:=B) (I:=M) (J:=J) (K:=O2)); auto; intros. lapply (mediatrice_droite (A:=A) (B:=B) (I:=M) (J:=J) (K:=O1)); auto; intros. elim (existence_rotation_Ia A M (pisurdeux + - x)); intros K; intros. cut (A <> K); intros. cut (alignes A K O2); intros. cut (alignes A K O1); intros. elim (classic (alignes A K M)); intros. apply (concours_unique (A:=M) (B:=A) (A1:=J) (B1:=K) (I:=O2) (J:=O1)); auto. apply orthogonal_non_alignes; auto. lapply (mediatrice_orthogonale_segment (A:=A) (B:=B) (M:=M) (N:=J)); auto; intros. elim (orthogonal_segment_milieu (A:=A) (B:=B) (C:=M) (D:=J) (I:=M)); auto; intros. auto with geo. apply ortho_sym. apply H35; auto. apply milieu_mediatrice; auto. apply permute_alignes; auto. apply permute_alignes; auto. apply (concours_unique (A:=A) (B:=M) (A1:=K) (B1:=J) (I:=O2) (J:=O1)); auto. assert (alignes M J O2); auto with geo. assert (alignes M J O1); auto with geo. discrimine K O1. apply alignes_angle; [ auto | auto | idtac ]. unfold double_AV in |- *. replace (cons_AV (vec A K) (vec A O1)) with (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A M) (vec A O1))). generalize (somme_triangle (A:=O1) (B:=A) (C:=B)); intros. generalize (isocele_angles_base (A:=O1) (B:=A) (C:=B)); auto; intros. generalize (angles_milieu (A:=O1) (B:=A) (C:=B) (I:=M)); auto; intros. rewrite <- H36; auto. replace (plus (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A B) (vec A O1))) (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A B) (vec A O1)))) with (plus (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A K) (vec A M))) (plus (cons_AV (vec A B) (vec A O1)) (cons_AV (vec A B) (vec A O1)))). replace (plus (cons_AV (vec A B) (vec A O1)) (cons_AV (vec A B) (vec A O1))) with (plus (image_angle pi) (opp (cons_AV (vec O1 A) (vec O1 B)))). rewrite def_opp; auto. rewrite <- (mes_oppx (A:=O1) (B:=A) (C:=O1) (D:=B) (x:=x + x)); auto. rewrite <- (mes_oppx (A:=A) (B:=M) (C:=A) (D:=K) (x:=pisurdeux + - x)); auto. repeat rewrite <- add_mes_compatible. replace pi with (pisurdeux + pisurdeux); auto. replace (- (pisurdeux + - x) + - (pisurdeux + - x) + (pisurdeux + pisurdeux + - (x + x))) with 0; auto. ring. elim (rotation_def (I:=A) (A:=M) (B:=K) (a:=pisurdeux + - x)); auto. rewrite <- H20; auto. rewrite <- H1; unfold double_AV in |- *. rewrite <- H16. rewrite add_mes_compatible; auto. rewrite <- H34; auto. rewrite <- H35; auto. mesure A B A O1. mesure O1 A O1 B. replace (x1 + (x0 + x0) + - x1) with (x0 + x0); auto. ring. mesure A K A M. mesure A B A O1. replace (x0 + x0 + (x1 + x1)) with (x0 + x1 + (x0 + x1)); auto. ring. rewrite Chasles; auto. discrimine K O2. apply alignes_angle; [ auto | auto | idtac ]. unfold double_AV in |- *. replace (cons_AV (vec A K) (vec A O2)) with (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A M) (vec A O2))). generalize (somme_triangle (A:=O2) (B:=A) (C:=B)); intros. generalize (isocele_angles_base (A:=O2) (B:=A) (C:=B)); auto; intros. generalize (angles_milieu (A:=O2) (B:=A) (C:=B) (I:=M)); auto; intros. rewrite <- H35; auto. replace (plus (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A B) (vec A O2))) (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A B) (vec A O2)))) with (plus (plus (cons_AV (vec A K) (vec A M)) (cons_AV (vec A K) (vec A M))) (plus (cons_AV (vec A B) (vec A O2)) (cons_AV (vec A B) (vec A O2)))). replace (plus (cons_AV (vec A B) (vec A O2)) (cons_AV (vec A B) (vec A O2))) with (plus (image_angle pi) (opp (cons_AV (vec O2 A) (vec O2 B)))). rewrite def_opp; auto. rewrite <- (mes_oppx (A:=O2) (B:=A) (C:=O2) (D:=B) (x:=x + x)); auto. rewrite <- (mes_oppx (A:=A) (B:=M) (C:=A) (D:=K) (x:=pisurdeux + - x)); auto. repeat rewrite <- add_mes_compatible. replace pi with (pisurdeux + pisurdeux); auto. replace (- (pisurdeux + - x) + - (pisurdeux + - x) + (pisurdeux + pisurdeux + - (x + x))) with 0; auto. ring. elim (rotation_def (I:=A) (A:=M) (B:=K) (a:=pisurdeux + - x)); auto. rewrite <- H19; auto. unfold double_AV in |- *. rewrite <- H16. rewrite add_mes_compatible; auto. rewrite <- H33; auto. rewrite <- H34; auto. mesure A B A O2. mesure O2 A O2 B. replace (x1 + (x0 + x0) + - x1) with (x0 + x0); auto. ring. mesure A K A M. mesure A B A O2. replace (x0 + x0 + (x1 + x1)) with (x0 + x1 + (x0 + x1)); auto. ring. rewrite Chasles; auto. apply image_distinct_centre with (2 := H30); auto. red in |- *; intros; apply H2. apply alignes_ordre_cycle; auto. apply alignes_angle; auto. Qed.