proposition: Lemma trianglesSD_proportion : forall A B C A' B' C' :PO, trianglesSD A B C A' B' C' -> exists k:R, distance B C =k*distance B' C' /\ distance A B = k*distance A' B' /\ distance A C = k * distance A' C'/\ k<>0.
proof: Proof. intros A B C A' B' C' H. generalize H;intro H1. destruct H1 as [H2 [H3 [H4 H5]]]. elim (@tout_angle_a_une_mesure A' B' A B); [intros |deroule_triangle A' B' C';auto|deroule_triangle A B C;auto]. set (M:=(rotation A' x B')). assert (H6 := refl_equal M); unfold M at 2 in H6. set (N:=(rotation A' x C')). assert (H7 := refl_equal N); unfold N at 2 in H7. assert (H8 : A' = rotation A' x A') by (apply rotation_def_centre;auto). assert ( H9: trianglesSD A' B' C' A' M N) by ( apply triangle_rotation_trianglesSD with (I := A') (a:=x);auto). set (B'':=(translation A' A M)). assert (H10 := refl_equal B''); unfold B'' at 2 in H10. set (C'':=(translation A' A N)). assert (H11:= refl_equal C''); unfold C'' at 2 in H11. assert (H12 : A = translation A' A A') by (apply rec_translation_vecteur;auto). assert ( H13: trianglesSD A' M N A B'' C''). apply (@triangle_translation_trianglesSD A' A);auto. destruct H9 as [H' [H'' _]];intros;auto. assert (H14 :trianglesSD A B C A B'' C'' ). apply (@trianglesS_trans_DD A B C A' M N A B'' C'');auto. apply (@trianglesS_trans_DD A B C A' B' C' A' M N);auto. assert (H15 : distance B' C' = distance B'' C''). rewrite <-(@rotation_isometrie A' B' C' M N x);auto. rewrite <-(@translation_isometrie A' A M B'' N C'');auto. assert (H16 :distance A' B' = distance A B''). rewrite <-(@rotation_isometrie A' A' B' A' M x);auto. rewrite <-(@translation_isometrie A' A A' A M B'');auto. assert (H17:distance A' C' = distance A C''). rewrite <-(@rotation_isometrie A' A' C' A' N x);auto. rewrite <-(@translation_isometrie A' A A' A N C'');auto. rewrite H15;rewrite H16;rewrite H17. generalize H14;intros H80. destruct H80 as [H' [H'' _]];intros;auto. deroule_triangle A B C. deroule_triangle A' B' C'. deroule_triangle A B'' C''. assert (cons_AV (vec A' B') (vec A B'') = image_angle x). rewrite <-(@translation_bipoint A' A A' A M B'');auto. elim (@rotation_def A' B' M x);auto with geo. rewrite H0 in H27. assert (cons_AV (vec A B'') (vec A B) =image_angle 0). rewrite <-(@Chasles_diff A' B');auto. rewrite H27. rewrite def_opp;auto. rewrite Chasles;auto. rewrite <- (@angle_nul);auto. elim (@trianglesSD_angles_cotes A B C A B'' C'');auto;intros . destruct H29 as [H81 [H82 H83]]. rewrite H81 in H28. rewrite H28 in H81. rewrite H28 in H82. rewrite H28 in H83. cut (alignes A B'' B);intros. cut (alignes A C'' C); intros . apply Thales_consequence;auto. apply imageZeroPi_paralelles;auto. assert (H84 :cons_AV(vec A C'') (vec A C) = cons_AV (vec C'' A)(vec C A)) by (apply angle_oppu_oppv;auto). rewrite H83 in H84. elim (@angle_nul_positif_colineaire A C'' C);[ intros k [_ H85]|auto|auto|auto]. unfold alignes;right. apply colineaire_alignes1 with (k:=k);auto. elim (@angle_nul_positif_colineaire A B'' B);[ intros k [_ H86]|auto|auto|auto]. unfold alignes;right. apply colineaire_alignes1 with (k:=k);auto. Qed.