proposition: Lemma positifColineaire_orient_inv_l: forall (A B C M :PO), orient A B C -> orient A M C -> alignes A B M -> positifColineaire A B M.
proof: Proof. intros A B C M H H0 H1 . destruct H1 as [H2|H3]. deroule_orient H. elim H4;auto. assert (H2: col_vec A B A M) by (apply alignes1_colineaire;auto). destruct H2 as [k H4]. destruct (@total_order_T k 0) as [[H1 | H1] |H1]. assert(orient A C M). apply negatifColineaire_orient_l with (B:=B);auto. exists k; deroule_orient H;auto. destruct (orient_compensation C M A);elim H5;apply orient_cycle;auto. assert ( A = M) by (apply (@produit_zero_conf k A M A B);auto). deroule_orient H0. elim H7;auto. unfold positifColineaire. exists k;repeat split;auto. deroule_orient H;auto. Qed.