proposition: Lemma sams_dec : forall A B C D E F, SAMS A B C D E F \/ ~ SAMS A B C D E F.
proof: Proof. intros A B C D E F. destruct(eq_dec_points A B). subst; right; intro; assert_diffs; auto. assert(HA' := symmetric_point_construction A B). destruct HA' as [A']. assert_diffs. destruct(lea_dec D E F C B A') as [|HNlea]. left; apply (sams_chara _ _ _ _ _ _ A'); Between. right. intro. apply HNlea, (sams_chara A); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles