proposition: Lemma negatifColineaire_orient_inv_l: forall (A B C M :PO), orient A B C -> orient A C M->alignes A B M-> negatifColineaire A B M.
proof: Proof. intros A B C M H H0 H1. destruct H1 as [H2|H2]. deroule_orient H. elim H4;auto. destruct (@alignes1_colineaire A B M) as [k H3];auto. destruct (@Rtotal_order k 0) as [H4 |[H4|H4]]. exists k;deroule_orient H;auto. rewrite H4 in H3. assert ( A =M) by (apply (@produit_zero_conf 0 A M A B);auto). deroule_orient H0. elim H9;auto. assert (H5 : orient A M C). apply (@positifColineaire_orient_l A B C M ); auto. exists k;deroule_orient H;auto. elim (@orient_compensation A M C);intros H6;elim H6; [auto |apply orient_cycle;apply orient_cycle;auto]. Qed.