proposition: Theorem Ptolemee: forall (A B C D : PO), orient A B C -> orient A B D -> orient C D A -> orient C D B -> sont_cocycliques A B C D -> (distance A B * distance C D ) + (distance B C *distance D A) = distance A C * distance B D.
proof: Proof. intros A B C D H0 H1 H2 H3 H4. assert ( H5: A<>B /\ A<>C /\ ~alignes A B C). deroule_orient H0;repeat split;auto. destruct H5 as [H5 [H6 H7]]. assert ( H8: A<>B /\ A<>D /\ ~alignes A B D). deroule_orient H1;repeat split;auto. destruct H8 as [H8 [H9 H10]]. assert ( H11: C<>D /\ C<>A /\ ~alignes C D A). deroule_orient H2;repeat split;auto. destruct H11 as [H11 [H12 H13]]. assert ( H14: C<>D /\ C<>B /\ ~alignes C D B). deroule_orient H3;repeat split;auto. destruct H14 as [H14 [H15 H16]]. destruct (@Exists_Intersection C D B A) as [E [H17 [H18 H19]]]. unfold vecEntreDeuxVec. left. split;auto. split;auto. apply orient_cycle;apply orient_cycle;auto. assert (H20 : E<>C). red;intro. rewrite H in H18. destruct H18 as [k [_ [H20 _]]]. assert (alignes D B C) by (apply (@colineaire_alignes k);auto). assert (alignes C D B) by (apply alignes_ordre_cycle2 ;auto). elim H16;auto. assert (H21 : cons_AV (vec C E) (vec C B) = cons_AV (vec C D) (vec C A)). rewrite <-(@Chasles C E C A C B);auto. rewrite <-H17. rewrite (plus_commutative). rewrite Chasles ;auto. assert (H40 : E<>D). red;intros. rewrite H in H17. rewrite <-angle_nul in H17; auto. destruct (@angle_nul_positif_colineaire C A B ) as [k [H41 H42]];auto. assert (alignes C A B ) by (apply (@colineaire_alignes k);auto). assert (alignes A B C) by (apply alignes_ordre_cycle ;auto). elim H7;auto. assert (H41 : E<>B). red;intros. rewrite H in H21. rewrite <-angle_nul in H21; auto. destruct (@angle_nul_positif_colineaire C D A ) as [k [H41 H42]];auto. assert (alignes C D A ) by (apply (@colineaire_alignes k);auto). elim H13;auto. assert (H22 : cons_AV (vec D E) (vec D C) = cons_AV (vec A B )(vec A C)). destruct H18 as [k [H22 [H23 H24]]]. rewrite H23. rewrite (@angle_produit_positif_l k D B D C);auto. apply consAD_orient_consAV;auto. apply cocyclicite;auto with geo. apply sont_cocycliques_avec_ordre_cycle;auto. apply orient_cycle;auto. assert (H23:cons_AV (vec A C) (vec A D) = cons_AV (vec B C )(vec B E)). destruct H19 as [k [H23 [H24 H25]]]. rewrite H24. rewrite (@angle_produit_positif_r2 k B D B C);auto. apply consAD_orient_consAV;auto. apply cocyclicite;auto with geo. apply sont_cocycliques_avec_ordre_cycle. apply sont_cocycliques_avec_ordre_cycle;auto. apply orient_cycle;apply orient_cycle;auto. apply orient_cycle;apply orient_cycle;auto. assert ( H24 : trianglesSD E C D B C A ). unfold trianglesSD. repeat split ;auto with geo. unfold triangle. red;intros. destruct H18 as [k [_ [H24 H25]]]. assert (alignes D B E) by (apply (@colineaire_alignes k);auto). assert (alignes E D B) by (apply alignes_ordre_cycle2;auto). assert (alignes E D C) by (apply alignes_ordre_permute;auto). assert (alignes D B C) by (apply alignes_trans2 with (A :=E);auto). assert (alignes C D B) by (apply alignes_ordre_cycle2;auto). elim H16;auto. assert ( H25 : trianglesSD E B C D A C ). unfold trianglesSD. repeat split ;auto with geo. unfold triangle. red;intros. destruct H19 as [k [_ [H25 H26]]]. assert (alignes B D E) by (apply (@colineaire_alignes k);auto). assert (alignes E B D) by (apply alignes_ordre_cycle2;auto). assert (alignes B C D) by (apply alignes_trans2 with (A :=E);auto). assert (alignes C D B) by (apply alignes_ordre_cycle;auto). elim H16;auto. destruct (@trianglesSD_proportion E C D B C A H24) as [k [H26 [H27 [H28 H29]]]]. assert (H30: distance E D * distance C A =distance B A * distance C D). rewrite H26. rewrite H28. ring. rewrite (@distance_sym C A) in H30. rewrite (@distance_sym B A) in H30. destruct (@trianglesSD_proportion E B C D A C H25) as [k' [H31 [H32 [H33 H34]]]]. assert (H35: distance E B * distance A C =distance B C * distance D A). rewrite H32. rewrite H31. ring. rewrite (@distance_sym E B) in H35. assert (H36 : distance B D = distance B E + distance E D) by (apply (@EntreDeuxPoint B D E H19 H18)). rewrite H36. rewrite <-H30. rewrite <-H35. ring. Qed.