proposition: Lemma conga_inangle2_per__acute : forall A B C P Q, Per A B C -> InAngle P A B C -> CongA P B A P B C -> InAngle Q A B C -> Acute P B Q.
proof: Proof. intros A B C P Q HPer HP1 HP2 HQ. assert (HP' := l11_24 P A B C HP1). assert (HQ' := l11_24 Q A B C HQ). assert (Hd := inangle_distincts A B C P HP1); assert (Hd' := inangle_distincts A B C Q HQ); spliter; clean. assert (HNCol : ~ Col A B C) by (apply per_not_col; auto). assert (HAcute : Acute A B P) by (apply conga_inangle_per__acute with C; assumption). assert (HNCol1 : ~ Col P B A). intro. assert (Col P B C) by (apply (col_conga_col P B A); assumption). apply HNCol; ColR. assert (HNCol2 : ~ Col P B C) by (apply (ncol_conga_ncol P B A); assumption). assert (~ Bet A B C) by (intro; apply HNCol; Col). destruct (col_dec B A Q). assert (Out B A Q) by (apply col_in_angle_out with C; Col). apply (acute_conga__acute A B P); trivial. apply conga_left_comm, out2__conga; [apply out_trivial|apply l6_6]; auto. destruct (col_dec B C Q). assert (Out B C Q) by (apply col_in_angle_out with A; Between; Col). apply (acute_conga__acute A B P); trivial. apply conga_left_comm, l11_10 with P A P C; try (apply out_trivial); auto. apply l6_6; assumption. destruct (col_dec B P Q). apply out__acute, col_inangle2__out with A C; assumption. destruct (cop__one_or_two_sides B P A Q) as [HOS|HTS]; Col. apply coplanar_perm_2, coplanar_trans_1 with C; Cop; Col. - apply acute_lea_acute with P B C. apply (acute_conga__acute A B P); try (apply conga_left_comm); assumption. exists Q; split; [|apply conga_refl; auto]. apply os2__inangle; apply invert_one_side. exists A; split; Side; apply in_angle_two_sides; Col. apply one_side_transitivity with A; [|apply one_side_symmetry]; apply in_angle_one_side; Col. - apply acute_lea_acute with A B P; trivial. apply lea_comm. exists Q; split; [|apply conga_pseudo_refl; auto]. apply os2__inangle; trivial. apply invert_one_side, one_side_transitivity with C; [|apply one_side_symmetry]; apply in_angle_one_side; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2