proposition: Lemma EntreDeuxPoint : forall ( A B M :PO), positifColineaire A B M -> positifColineaire B A M -> distance A B = distance A M + distance M B.
proof: Proof. intros A B M H0 H1. destruct H0 as [k [H2 [H3 H4]]]. destruct H1 as [k' [H5 [H6 H7]]]. assert (vec M B = mult_PP k' (vec A B)). rewrite (@opp_vecteur B A). rewrite ->mult_mult_vec. rewrite (@opp_vecteur B M). rewrite H6. rewrite ->mult_mult_vec. replace (-1 * k') with (k' *-1);auto. ring. assert (H8: vec A B = add_PP (vec A M)(vec M B)). symmetry. apply (@Chasles_vec A M B) ;auto. rewrite H3 in H8. rewrite H in H8. replace ( add_PP(mult_PP k(vec A B)) (mult_PP k' (vec A B))) with (mult_PP (k+k')(vec A B)) in H8;[idtac|RingPP]. assert (H9: add_PP (mult_PP (k+k') (vec A B)) (mult_PP (-1) (vec A B)) = zero). rewrite <-H8. rewrite <-opp_vecteur. rewrite Chasles_vec. unfold vec. rewrite add_PP_A. replace (-1+1) with 0. rewrite<-def_zero;auto. ring. replace ( add_PP(mult_PP (k+k') (vec A B)) (mult_PP (-1) (vec A B))) with (mult_PP (k+k'+-1)(vec A B)) in H9;[idtac|RingPP]. elim (@produit_vecteur_nul (k+k'+-1) A B H9);intros H10. assert ( H11 : distance A M = Rabs k *distance A B) by (apply (@colinearite_distance k A B A M H3)) . assert ( H12 : distance M B = Rabs k' *distance A B) by (apply (@colinearite_distance k' A B M B H)) . rewrite Rabs_right in H11;[idtac|lra]. rewrite Rabs_right in H12;[idtac|lra]. rewrite H11. rewrite H12. rewrite<-Rmult_plus_distr_r. assert (k+k' =1). auto with *. rewrite H0; ring. elim H2;auto. Qed.