proposition: Lemma negatifColineaire_orient_inv_r: forall (A B C M :PO), orient A B C -> orient A M B->alignes A C M-> negatifColineaire A C M.
proof: Proof. intros A B C M H H0 H1. destruct H1 as [H2|H2]. deroule_orient H. elim H6;auto. destruct (@alignes1_colineaire A C 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 C);auto). deroule_orient H0. elim H7;auto. assert (H5 : orient A B M ). apply (@positifColineaire_orient_r A B C M ); auto. exists k;deroule_orient H; auto. elim (@orient_compensation A B M );intros H6;elim H6; [auto |apply orient_cycle;apply orient_cycle;auto]. Qed.