proposition: Lemma conga_inangle_per__acute : forall A B C P, Per A B C -> InAngle P A B C -> CongA P B A P B C -> Acute A B P.
proof: Proof. intros A B C P HPer HP1 HP2. assert (Hd := inangle_distincts A B C P HP1); spliter; clean. assert (HNCol : ~ Col A B C) by (apply per_not_col; auto). exists A, B, C; split; trivial. split. apply inangle__lea, HP1. intro Habs. assert (Per A B P) by (apply l11_17 with A B C, conga_sym; trivial). apply HNCol, col_permutation_1, cop_per2__col with P; Cop. apply l11_17 with A B P; trivial. apply conga_comm, HP2. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2