proposition: Lemma vecEntreDeuxVec_intersection_middle2: 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 B C M /\ positifColineaire C B M.
proof: Proof. intros A B C D H H0 M [H2 H1]. elim H0;intros [H3 [H4 H5]]. assert (positifColineaire A D M) by (apply(@vecEntreDeuxVec_intersection_middle1 A B C D );auto). assert (orient A B M) by (apply positifColineaire_orient_r with (C:=D);auto). assert (orient A M C) by (apply positifColineaire_orient_l with (B:=D);auto). split. apply (@positifColineaire_orient_inv_l B C A M);auto. apply orient_cycle;assumption. apply orient_cycle;assumption. apply (@positifColineaire_orient_inv_r C A B M);auto. apply orient_cycle;apply orient_cycle;assumption. apply orient_cycle;apply orient_cycle;assumption. apply permute_alignes;assumption. destruct (@orient_compensation A B C) as [H6|H6]. elim H6;auto. elim H6;apply orient_cycle;apply orient_cycle;auto. Qed.