proposition: Lemma Exists_Intersection1 : forall (A B C D :PO), vecEntreDeuxVec A B C D -> exists E :PO, alignes A D E /\ alignes B C E.
proof: Proof. intros A B C D H. assert (H0 : ~alignes A D B /\ A <>D) by(destruct H as [[_ [H2 _]]|[_ [_ H2]]];deroule_orient H2;auto with geo). destruct H0 as [H0 H1]. assert (H2 : ~alignes A D C) by(destruct H as [[_ [_ H3 ]]|[_ [H3 _]]];deroule_orient H3;auto with geo). assert (H3 : B<>C) by(destruct H as [[H4 [_ _]]|[H4 [_ _]]];deroule_orient H4;auto with geo). destruct (@existence_pt_intersection A D B C ) as [E H4];auto. assert (H4: ~ paralleles (droite A D) (droite B C)). red;intros H4. destruct (@existence_representant_vecteur A B C) as [D' H5]. destruct (@paralleles_vecteur A D B C ) as [k H6];auto. destruct H as [[H7 [H8 H9]]|[H7 [H8 H9]]]. assert (aire(vec B C)(vec A D) = 0) by (apply aire_colinearite with (k:=k) ;auto). rewrite <-(@Chasles_vec B A C) in H. rewrite aire_distrib_r in H. assert (aire (vec B A)(vec A D) <0). VReplace (vec B A) (mult_PP (-1) (vec A B)). rewrite aire_colineaire_l. unfold orient in H8;lra. assert (aire (vec A C)(vec A D) <0). rewrite aire_anti_symetrique. unfold orient in H9;lra. lra. assert (aire(vec B C)(vec A D) = 0) by (apply aire_colinearite with (k:=k) ;auto). rewrite <-(@Chasles_vec B A C) in H. rewrite aire_distrib_r in H. assert (aire (vec B A)(vec A D) >0). VReplace (vec B A) (mult_PP (-1) (vec A B)). rewrite aire_colineaire_l. rewrite aire_anti_symetrique. unfold orient in H9. replace (-1) with (-(1)) by ring. rewrite Ropp_mult_distr_l_reverse. rewrite Ropp_mult_distr_r_reverse. lra. assert (aire (vec A C)(vec A D) >0). unfold orient in H8;auto. lra. elim (@droites_non_paralleles B C A D H3 H1 H4);auto. intros H5. assert (H6: coplanaires B C A D) by apply geometrie_plane. elim H5;auto. exists E;auto. apply def_pt_intersection2;auto. Qed.