proposition: Lemma ts__suma : forall A B C D, TS A B C D -> SumA C B A A B D C B D.
proof: Proof. intros A B C D HTS. exists D. assert_diffs. split; CongA. split; Side. split; CongA; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles