proposition: Lemma alignes_positifColineaire : forall ( A B M :PO), A<>B ->alignes A B M -> positifColineaire A B M \/ positifColineaire B A M.
proof: Proof. intros A B M H H0. elim H0;intros H1. elim H;auto. assert (H2: col_vec A B A M) by (apply alignes1_colineaire;auto). elim H2;intros k H3. elim (Rle_or_lt k 0);intro H4. assert ( H5 : vec B M =mult_PP (1-k) (vec B A)). rewrite <-(Chasles_vec B A M) . rewrite ->(opp_vecteur A B) . rewrite H3. rewrite (mult_mult_vec A B (1-k) (-1)). replace ((1-k)* -1) with (k-1); [idtac | ring]. assert (H6: add_PP (mult_PP (-1) (vec A B))(mult_PP k (vec A B))= mult_PP (-1 +k) (vec A B )) by RingPP. rewrite H6. replace (-1 + k ) with (k-1);[auto|ring]. assert (H7: 1-k >0). lra. right;unfold positifColineaire. exists (1-k);auto. left;unfold positifColineaire. exists k;auto. Qed.