proposition: Lemma Thales_consequence : forall A B C M N :PO, triangle A B C -> triangle A M N -> alignes A M B -> alignes A N C -> paralleles (droite M N) (droite B C)-> exists k:R, distance B C = k* distance M N /\ distance A B = k* distance A M /\ distance A C = k * distance A N /\ k<>0.
proof: Proof. intros A B C M N H0 H1 H2 H3 H. deroule_triangle A B C. deroule_triangle A M N. halignes H2 k. assert (vec A M = mult_PP (/k) (vec A B)). apply (@inversion_colineaire k A M B H7 H12). assert (k<>0). red;intros. rewrite H14 in H12. unfold vec at 2 in H12 . assert(mult_PP 0 (add_PP(cons(-1) A)(cons 1 M) ) = zero) by RingPP. rewrite H15 in H12. assert (A=B) by apply (@vecteur_nul_conf A B H12) . elim H7;auto. assert (/k<>0) by apply (@Rinv_neq_0_compat k H14). assert (vec A N = mult_PP (/k) (vec A C)) by (apply (@Thales_concours (/k) A B C M N H0 H15 H13);auto with geo). assert (vec A C = mult_PP (k) (vec A N)) . elim (@Rinv_inv k);auto. apply (@inversion_colineaire (/k) A C N );auto. assert (vec B C =mult_PP (k) (vec M N)). rewrite <-(@Chasles_vec M A N). rewrite <- distrib_mult_PP . rewrite <-H17 . assert ( vec B A = mult_PP (k) (vec M A)). rewrite(@opp_vecteur A M ). rewrite mult_mult_vec . replace (k * -1) with (-1 * k). rewrite <-mult_mult_vec . rewrite <-H12. apply opp_vecteur;auto. ring. rewrite <-H18. rewrite Chasles_vec;auto. exists (Rabs(k)). repeat split; [apply colinearite_distance;auto |apply colinearite_distance;auto| apply colinearite_distance;auto|apply Rabs_no_R0;auto]. Qed.