proposition: Lemma trianglesS_trans_II: forall A B C A' B' C' M N P :PO, trianglesSI A B C A' B' C' -> trianglesSI 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 . assert (H31: cons_AV (vec B' A') (vec B' C') = cons_AV (vec N P)(vec N M)) by (apply permute_angles ;auto). assert (H32: cons_AV (vec C' B') (vec C' A') = cons_AV (vec P M)(vec P N)) by (apply permute_angles ;auto). rewrite H31 in H15. rewrite H32 in H18. unfold trianglesSD; auto. Qed.