proposition: Lemma conga_cop_inangle_per2__inangle : forall A B C P T, Per A B C -> InAngle T A B C -> CongA P B A P B C -> Per B P T -> Coplanar A B C P -> InAngle P A B C.
proof: Proof. intros A B C P T HPer HInangle HConga HPerP HCop. destruct (eq_dec_points P T). subst; apply HInangle. assert_diffs. destruct (angle_bisector A B C) as [P' [HInangle' HConga']]; auto. assert_diffs. assert (HAcute : Acute P' B A). apply acute_sym, conga_inangle_per__acute with C; trivial. apply l11_25 with P' A C; try (apply out_trivial); auto. assert (HNCol1 : ~ Col A B C) by (apply per_not_col; auto). assert (HCol : Col B P P'). apply conga2_cop2__col with A C; trivial. intro; apply HNCol1; Col. apply coplanar_trans_1 with C; Cop; Col. apply coplanar_trans_1 with A; Cop. apply (acute_col_perp__out T); Col. { apply acute_lea_acute with P' B A; trivial. assert (HNCol2 : ~ Col P' B A). intro. assert (Col P' B C) by (apply (col_conga_col P' B A); assumption). apply HNCol1; ColR. assert (Coplanar A B T P') by (apply coplanar_trans_1 with C; Cop; Col). destruct (col_dec T B P'); [|assert_diffs; destruct (cop__one_or_two_sides B P' A T); Col; Cop]. - apply l11_31_1; auto. apply col_one_side_out with A; Col. apply invert_one_side, inangle_one_side with C; Col. assert (~ Col B P T) by (apply per_not_col; auto). intro; assert_diffs; apply HNCol2; ColR. - apply (l11_30 P' B T P' B C); CongA. apply inangle__lea, (in_angle_trans2 A); trivial. apply os_ts__inangle; trivial. apply invert_one_side, inangle_one_side with C; Col. intro; apply HNCol1, bet_col, bet_in_angle_bet with T; trivial. apply col_two_sides_bet with P'; Col. - apply lea_left_comm, inangle__lea. destruct (col_dec B A T). apply out341__inangle; auto. apply col_one_side_out with P'; assumption. apply os2__inangle; trivial. apply invert_one_side, inangle_one_side with C; Col. } apply perp_col with P; Col. apply perp_right_comm, per_perp; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles