proposition: Lemma triangles_semblables_proportion : forall A B C A' B' C' :PO, triangles_semblables 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. unfold triangles_semblables in H. elim H;intros H1. apply trianglesSD_proportion ;auto. apply trianglesSI_proportion ;auto. Qed.