proposition: Lemma angle_bisector : forall A B C, A <> B -> C <> B -> exists P, InAngle P A B C /\ CongA P B A P B C.
proof: Proof. intros A B C HAB HCB. elim (col_dec A B C). { intro HCol. elim (bet_dec A B C). - intro HBet; destruct (not_col_exists A B) as [Q HNCol]; trivial. destruct (l10_15 A B B Q) as [P [HPerp HOS]]; Col. assert_diffs; exists P; split. apply in_angle_line; auto. apply l11_18_1; Perp. - intro HOut; apply not_bet_out in HOut; trivial; assert_diffs. exists C; split. repeat split; auto. exists C; split; Between. right; apply out_trivial; auto. apply l11_21_b. apply l6_6; trivial. apply out_trivial; auto. } intro HNCol. assert_diffs. destruct (l6_11_existence B B A C) as [C0 [HOut HCong]]; auto. destruct (midpoint_existence A C0) as [P HP]. exists P. assert_diffs. assert (HNCol1 : ~ Col A B C0) by (intro; apply HNCol; ColR). assert_diffs. assert (P <> B) by (intro; subst P; apply HNCol1; Col). split. apply (l11_25 P A B C0); try (apply out_trivial); auto; [|apply l6_6; trivial]. repeat split; auto. exists P; split; Between. right; apply out_trivial; auto. destruct (l11_51 B P A B P C0); Cong. apply (l11_10 P B A P B C0); try (apply out_trivial); auto; apply l6_6; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2