proposition: Lemma vecEntreDeuxVec_intersection_left2: forall ( A B C D :PO), vecEntreDeuxVec A B C D -> forall M :PO, alignes A B M /\ alignes C D M -> (negatifColineaire C D M -> negatifColineaire A B M) /\ (negatifColineaire A B M -> negatifColineaire C D M).
proof: Proof. intros A B C D H M [H3 H2]. repeat split;intro H1. destruct H as [[H19 [H20 H21]] |[H19 [H20 H21]]]. assert (H4 : orient A C M). apply orient_cycle;apply orient_cycle. apply negatifColineaire_orient_r with (C:=D);auto. apply orient_cycle;apply orient_cycle;auto. apply negatifColineaire_orient_inv_l with (C:=C);auto. assert (H4 : orient A M C ). apply orient_cycle. apply negatifColineaire_orient_l with (B:=D);auto. apply orient_cycle;auto. apply negatifColineaire_orient_inv_r with (B:=C);auto. destruct H as [[H19 [H20 H21]] |[H19 [H20 H21]]]. assert (H4 : orient C M A ). apply orient_cycle. apply negatifColineaire_orient_l with (B:=B);auto. apply negatifColineaire_orient_inv_r with (B:=A);auto. apply orient_cycle;apply orient_cycle;auto. assert (H4 : orient C A M ). apply orient_cycle;apply orient_cycle. apply negatifColineaire_orient_r with (C:=B);auto. apply negatifColineaire_orient_inv_l with (C:=A);auto. apply orient_cycle;auto. Qed.