proposition: Theorem SommeAnglesInscritsOriente: forall (A B C D : PO), sont_cocycliques A B C D ->orient A B C -> orient A C D -> orient A B D.
proof: Proof. intros A B C D H H0 H1. destruct (@position_3points_2 A B D) as [H2|[H2|H2]];auto. assert (H3:orient B C D). apply orient_4point with (D:=A);auto. apply orient_cycle;auto. apply orient_cycle;auto. apply orient_cycle;apply orient_cycle;auto. assert (H4:cons_AV(vec A D )(vec A B) = cons_AV (vec C D)(vec C B)). apply consAD_orient_consAV. apply cocyclicite;auto with geo. deroule_orient H2 ;auto with geo. deroule_orient H3 ;auto with geo. apply sont_cocycliques_avec_ordre_cycle. apply sont_cocycliques_avec_ordre_permute. apply sont_cocycliques_avec_ordre_cycle;apply sont_cocycliques_avec_ordre_cycle;auto. apply orient_cycle;auto. apply orient_cycle;auto. assert (H5:cons_AV(vec A B )(vec A C) = cons_AV (vec D B)(vec D C)). apply consAD_orient_consAV;auto. apply cocyclicite;auto with geo. deroule_orient H0 ;auto with geo. deroule_orient H3 ;auto with geo. apply sont_cocycliques_avec_ordre_permute. apply sont_cocycliques_avec_ordre_cycle;auto. apply orient_cycle;apply orient_cycle;auto. assert (H6:cons_AV(vec A C )(vec A D) = cons_AV (vec B C)(vec B D)). apply consAD_orient_consAV;auto. apply cocyclicite;auto with geo. deroule_orient H1 ;auto with geo. deroule_orient H3 ;auto with geo. apply sont_cocycliques_avec_ordre_cycle. apply sont_cocycliques_avec_ordre_cycle;auto. assert (plus (cons_AV (vec C D) (vec C B)) (plus (cons_AV (vec D B) (vec D C)) (cons_AV (vec B C) (vec B D))) = image_angle pi). apply somme_triangle;deroule_orient H3;auto. rewrite <-H4 in H7. rewrite <-H5 in H7. rewrite <-H6 in H7. rewrite Chasles in H7;(deroule_orient H0;deroule_orient H1;auto). rewrite Chasles in H7;(deroule_orient H0;deroule_orient H1;auto). rewrite <-angle_nul in H7;auto. elim differencePiNull;auto. assert (H3: col_vec A B A D) . apply alignes1_colineaire;auto with geo. unfold alignes in H2. elim H2;intros;auto. deroule_orient H0. elim H6;auto. destruct H3 as [k H4]. destruct (@total_order_T k 0) as [[H5| H5] |H5]. assert (H6: vec B D = mult_PP (1-k) (vec B A)). rewrite <-(@Chasles_vec B A D) . rewrite H4. VReplace (vec A B) (mult_PP (-1) (vec B A)). rewrite mult_mult_vec. replace (k*-1) with (-k);[idtac|ring]. replace (1-k) with (1+(-k));auto with real. VReplace (vec B A) (mult_PP (1) (vec B A)). RingPP. assert (H7: 1-k >0). lra. assert(H8 : orient D B C). apply orient_cycle;apply orient_cycle. apply positifColineaire_orient_r with (C:=A). apply orient_cycle;auto. exists (1-k);deroule_orient H0;auto. assert (H9:cons_AV(vec D B )(vec D C) = cons_AV (vec A B)(vec A C)). apply consAD_orient_consAV;auto. apply cocyclicite;auto with geo. deroule_orient H8 ;auto with geo. deroule_orient H0 ;auto with geo. apply sont_cocycliques_avec_ordre_cycle;auto. assert (trianglesSD C A B C D B ). repeat split. deroule_orient H0;auto with geo. deroule_orient H8;auto with geo. auto. rewrite (@angle_produit_positif_r (1-k) B A D B C ) ;auto. deroule_orient H0;auto with geo. deroule_orient H0;auto with geo. assert (cons_AV (vec C A)(vec C B) =cons_AV (vec C D)(vec C B)). apply (@trianglesSD_angles_egaux C A B C D B);auto. assert (cons_AV (vec C A) (vec C D) = image_angle 0). rewrite <-(@Chasles C A C B C D);(deroule_orient H0;deroule_orient H1;auto with geo). rewrite H10. rewrite Chasles;auto with geo. rewrite (@ angle_nul C D) ;auto. destruct (@angle_nul_positif_colineaire C A D) as [k' [H12 H13]];(deroule_orient H0;deroule_orient H1;auto). assert (alignes C A D) . apply colineaire_alignes with (k:=k');auto. elim H23. apply alignes_ordre_permute . apply alignes_ordre_cycle;auto. assert (A=D). apply (@produit_zero_conf k A D A B);auto. deroule_orient H1. elim H10;auto. assert (orient A D C). apply (@positifColineaire_orient_l A B C D H0);auto. exists k;deroule_orient H0;auto. elim (@orient_compensation D C A);intro. elim H6. apply orient_cycle;auto. elim H6. apply orient_cycle;auto. Qed.