proposition: Lemma acute2__sams : forall A B C D E F, Acute A B C -> Acute D E F -> SAMS A B C D E F.
proof: Proof. assert (Haux : forall A B C D E F, Acute A B C -> LeA D E F A B C -> SAMS A B C D E F). { intros A B C D E F HAcute HLea. apply sams_lea2__sams with A B C A B C. apply acute__sams, HAcute. assert_diffs; apply lea_refl; auto. assumption. } intros A B C D E F HAcute1 HAcute2. assert_diffs. destruct (lea_total A B C D E F); SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles