proposition: Lemma suppa__sams : forall A B C D E F, SuppA A B C D E F -> SAMS A B C D E F.
proof: Proof. intros A B C D E F [HAB [A' [HBet HCong]]]. assert_diffs. apply (conga2_sams__sams A B C C B A'); CongA. apply bet__sams; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles