proposition: Lemma conga__acute : forall A B C, CongA A B C A C B -> Acute A B C.
proof: Proof. intros A B C HCongA. destruct (col_dec A B C). { apply out__acute, not_bet_out; trivial. intro. absurd (B = C). apply conga_distinct in HCongA; spliter; auto. apply between_equality with A; apply between_symmetry; trivial. apply (bet_conga__bet A B C); assumption. } destruct (segment_construction C B C B) as [C' []]. apply conga_distinct in HCongA; spliter. assert_diffs. apply acute_sym, acute_chara with C'; auto. destruct (l11_41 B C A C'); Col. apply (conga_preserves_lta B C A A B C'); trivial. apply conga_comm, conga_sym; assumption. apply conga_pseudo_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2