proposition: Lemma vecEntreDeuxVec_intersection_middle1: forall ( A B C D :PO),orient A B C -> vecEntreDeuxVec A B C D -> forall M:PO, alignes A D M /\ alignes B C M -> positifColineaire A D M.
proof: Proof. intros A B C D H H0 M [H2 H1] . elim H0;intros [H3 [H4 H5]]. destruct H2 as [H2|H2]. deroule_orient H5;elim H8;auto. destruct (@alignes1_colineaire A D M) as [k H6];auto. destruct (@Rtotal_order k 0) as [H7|[H7|H7]]. assert (orient A C M) by (apply (@negatifColineaire_orient_l A D C M H5 );auto; exists k; deroule_orient H5;auto). assert (orient A M B) by (apply (@negatifColineaire_orient_r A B D M H4 );auto; exists k; deroule_orient H4;auto). assert (orient M B C). apply orient_4point with (D:=A);auto. apply orient_cycle; auto. apply orient_cycle;auto. apply orient_cycle;auto. deroule_orient H10. elim H14;apply alignes_ordre_cycle2;auto. assert (A=M) by (apply produit_zero_conf with (k:=k) (C:=A)(D:=D);auto). rewrite <-H8 in H1. deroule_orient H3. elim H12;auto with geo. exists k;repeat split;auto. deroule_orient H5;auto. destruct (@orient_compensation A B C) as [H6|H6]. elim H6;auto. elim H6;apply orient_cycle;apply orient_cycle;auto. Qed.