proposition: Lemma suma123231__sams : forall A B C D E F, SumA A B C B C A D E F -> SAMS D E F C A B.
proof: Proof. exact (t22_20 not_obtuse_saccheris). Qed.
imports: GeoCoq.Tarski_dev.Annexes.circles GeoCoq.Tarski_dev.Annexes.half_angles GeoCoq.Tarski_dev.Ch12_parallel_inter_dec