proposition: Lemma acute_suppa__obtuse : forall A B C D E F, Acute A B C -> SuppA A B C D E F -> Obtuse D E F.
proof: Proof. unfold SuppA. intros; spliter. ex_and H1 A'. apply (conga_obtuse__obtuse C B A'); [|apply conga_sym, H2]. apply conga_distinct in H2; spliter. apply obtuse_sym, (acute_bet__obtuse A); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2