proposition: Lemma vecEntreDeuxVec_intersection_middle: forall ( A B C D :PO), vecEntreDeuxVec A B C D -> forall M:PO, alignes A D M /\ alignes B C M -> positifColineaire B C M /\ positifColineaire C B M /\ positifColineaire A D M.
proof: Proof. intros A B C D H M [H1 H0]. elim H;intros [H2 [H3 H4]]. assert (positifColineaire B C M /\ positifColineaire C B M). apply (@vecEntreDeuxVec_intersection_middle2 A B C D );auto. assert (positifColineaire A D M). apply (@vecEntreDeuxVec_intersection_middle1 A B C D );auto. destruct H5 as [H7 H8]. split;auto. assert (vecEntreDeuxVec A C B D) by (unfold vecEntreDeuxVec;left;split;auto). assert (positifColineaire C B M /\ positifColineaire B C M). apply (@vecEntreDeuxVec_intersection_middle2 A C B D );auto with geo. assert (positifColineaire A D M). apply (@vecEntreDeuxVec_intersection_middle1 A C B D );auto with geo. destruct H6 as [H8 H9]. split;auto. Qed.