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