proposition: Lemma Exists_Intersection : forall (A B C D :PO), vecEntreDeuxVec A B C D -> exists E :PO, cons_AV ( vec A B) (vec A E) = cons_AV (vec A D) (vec A C) /\ positifColineaire B C E /\ positifColineaire C B E.
proof: Proof. intros A B C D H. assert (H1: A<>B /\ A<>C /\ A<>D). elim H;intros [H2[H3 H4]]; deroule_orient H2;deroule_orient H4;repeat split;auto. destruct H1 as [H1 [H2 H3]]. destruct (@existence_representant_unitaire A B) as [B' H4];auto. destruct(@existence_representant_cons (cons_AV (vec A D)(vec A C)) A B' A) as [E' [H5 H6]]. unfold distance. destruct (@def_representant_unitaire2 A B B' H1 H4) as [_ [H7 _]]. rewrite H7. rewrite sqrt_1;auto. assert (H7: A<>E'). red;intros. rewrite H0 in H5. assert (distance E' E' =0) by (apply distance_refl2;auto). rewrite H7 in H5. assert (1<>0) by lra. elim H8;auto. assert (H8 : cons_AV (vec A B)(vec A E') = cons_AV (vec A B') (vec A E')). rewrite H4. apply angles_representants_unitaires2;auto. rewrite <-H8 in H6. assert (H9 :cons_AV (vec A E')(vec A C) = cons_AV (vec A B)(vec A D)). rewrite <-(@Chasles A B A E' A D);auto. rewrite <-H6. rewrite plus_commutative. rewrite ->(@Chasles A E' A D A C);auto. assert (H10:vecEntreDeuxVec A B C E'). apply (@EntreDeuxVec_sym A B C D E');auto. destruct (@Exists_Intersection1 A B C E') as [E [H11 H12]];auto. exists E. destruct (@vecEntreDeuxVec_intersection_middle A B C E' H10 E ) as [H13 [H14 H15]];auto. repeat split;auto. destruct H15 as [k [H16[H17 H18]]]. rewrite (@angle_produit_positif_r k A E' E A B);auto. Qed.