proposition: Lemma trianglesS_trans_DI: forall A B C A' B' C' M N P :PO, trianglesSD A B C A' B' C' -> trianglesSI A' B' C' M N P-> trianglesSI A B C M N P.
proof: Proof. intros A B C A' B' C' M N P H H1. expand_triangles_semblables ;clear H . expand_triangles_semblables ;clear H1 . rewrite <-H3 in H15. rewrite <-H6 in H18. unfold trianglesSI; auto. Qed.