proposition: Lemma acute_trivial : forall A B, A <> B -> Acute A B A.
proof: Proof. intros. assert(HH:= not_col_exists A B H). ex_and HH P. assert(exists C : Tpoint, Per C B A /\ Cong C B A B /\ OS A B C P). apply(ex_per_cong A B B P A B H H); Col; exists A. ex_and H1 C. assert_diffs. exists A, B, C. split. apply l8_2. auto. split. exists A. split. apply inangle1123; auto. apply conga_refl; auto. intro. assert(Out B A C). apply(l11_21_a A B A A B C). apply out_trivial; auto. auto. assert(Perp C B B A). apply per_perp_in in H1; auto. apply perp_in_perp_bis in H1. induction H1. apply perp_not_eq_1 in H1. tauto. auto. apply perp_comm in H10. apply perp_not_col in H10. apply out_col in H8. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2