proposition: Lemma trianglesSI_proportion : forall A B C A' B' C' :PO, trianglesSI 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. expand_triangles_semblables. set (A'':=(reflexion B' C' A')). assert (H20 := refl_equal A''); unfold A'' at 2 in H20. assert (H21: B' = reflexion B' C' B') by (apply reflexion_axe;auto with geo). assert (H22: C' = reflexion B' C' C') by (apply reflexion_axe;auto with geo). assert (H23: trianglesSI A' B' C' A'' B' C') by (apply (@triangle_reflexion_trianglesSI B' C');auto). assert (H24 : distance A' B' = distance A'' B') by (apply (@reflexion_isometrie B' C');auto). assert (H25 : distance A' C' = distance A'' C') by (apply (@reflexion_isometrie B' C');auto). rewrite H24. rewrite H25. assert (H26: trianglesSD A B C A'' B' C') by (apply (@trianglesS_trans_II A B C A' B' C' A'' B' C');auto). apply trianglesSD_proportion;auto. Qed.