proposition: Lemma sams_assoc : forall A B C D E F G H I A' B' C' D' E' F', SAMS A B C D E F -> SAMS D E F G H I -> SumA A B C D E F A' B' C' -> SumA D E F G H I D' E' F' -> (SAMS A' B' C' G H I <-> SAMS A B C D' E' F').
proof: Proof. intros A B C D E F. split. apply (sams_assoc_1 _ _ _ D E F); auto. apply (sams_assoc_2 _ _ _ D E F); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles