proposition: Lemma acute__sams : forall A B C, Acute A B C -> SAMS A B C A B C.
proof: Proof. intros A B C Hacute. assert(HA' := symmetric_point_construction A B). destruct HA' as [A']. assert_diffs. apply (sams_chara _ _ _ _ _ _ A'); Between. apply acute_obtuse__lta; auto. apply obtuse_sym. apply (acute_bet__obtuse A); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles