proposition: Lemma out546__sams : forall A B C D E F, A <> B -> B <> C -> Out E D F -> SAMS A B C D E F.
proof: Proof. intros A B C D E F HAB HBC HOut. destruct (segment_construction A B A B) as [A' [HBet HCong]]. assert_diffs. apply sams_chara with A'; auto. apply l11_31_1; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles