proposition: Lemma acute_per__sams : forall A B C D E F, A <> B -> B <> C -> Per A B C -> Acute D E F -> SAMS A B C D E F.
proof: Proof. intros A B C D E F HAB HBC HPer HAcute. apply sams_lea2__sams with A B C A B C. apply per2__sams; auto. apply lea_refl; auto. apply acute_per__lta; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles