proposition: Lemma sams123231 : forall A B C, A <> B -> A <> C -> B <> C -> SAMS A B C B C A.
proof: Proof. intros A B C. intros. assert(HA' := symmetric_point_construction A B). destruct HA' as [A']. assert_diffs. apply (sams_chara _ _ _ _ _ _ A'); Between. elim(col_dec A B C). { intro HCol. elim(bet_dec A C B). { intro HCBet. apply conga__lea. apply conga_line; Between. apply (between_exchange3 A); Between. } intro. apply l11_31_1; auto. apply l6_6. apply not_bet_out; Col. } intro. apply lta__lea. apply l11_41_aux; Col; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles