proposition: Lemma bisector_existence : forall A B C, A <> B -> B <> C -> exists E, InAngle E A B C /\ CongA A B E E B C.
proof: Proof. intros A B C HAB HBC. destruct (col_dec A B C) as [HCOL | HNCOL]. destruct (out_dec B A C) as [HOUT | HNOUT]. exists C. split. Side. apply (l11_21_b A B C C B C);auto. apply (out_trivial B C);auto. assert (Bet A B C) by(apply (not_out_bet A B C);auto). destruct (perp_exists B A C) as [E HPerp]. intro HEQAC. subst. elim HAB. apply (between_identity C B); auto. exists E. split. assert_diffs. repeat split; auto. exists B. split;auto. assert (Perp B E A B) by (apply (perp_col1 B E A C B);Col). assert (Perp B E C B) by (assert_diffs;apply (perp_col1 B E C A B);Perp;Col). assert (Per E B A) by (apply (perp_per_1 B E A);assumption). assert (Per E B C) by (apply (perp_per_2 B E C);Perp). assert (CongA E B A E B C) by (assert_diffs;apply (l11_16 E B A E B C);auto). CongA. destruct (segment_construction B A B C ) as [C'[ HC'1 HC'2]]. destruct (segment_construction B C B A ) as [A' [HA'1 HA'2]]. destruct (midpoint_existence A' C') as [I HI]. assert (Cong B C' A' B) by (apply l2_11 with A C;Cong;Between). assert_diffs. assert (CongA A' C' B C' A' B). { apply (isosceles_conga C' B A');auto. { intro. subst. treat_equalities. assert_cols. apply HNCOL. ColR. } unfold isosceles. Cong. } assert (HTRI : Cong I B I B /\ (I <> B -> CongA C' I B A' I B /\ CongA C' B I A' B I)). { apply (l11_49 I C' B I A' B); Cong. assert_diffs. apply (l11_10 A' C' B C' A' B I B I B);Out. } exists I. destruct HTRI as [HCONGIB HIBO]. assert (I <> B) by (intro;elim HNCOL;ColR). assert (CongA A B I I B C). { apply (l11_10 C' B I I B A' A I I C);Out. apply conga_right_comm. apply HIBO;auto. } split. unfold InAngle. repeat split; auto. destruct (inner_pasch A' B C' I A) as [x1 HIN1]. apply (midpoint_bet A' I C');auto. Between. destruct HIN1 as [HIN11 HIN12]. destruct (inner_pasch A B A' x1 C) as [x2 HIN2];auto. exists x2. destruct HIN2 as [HIN21 HIN22]. split. apply (Bet_cases A x2 C). right;auto. right. apply (bet_out B x2 I). intro. elim HNCOL;ColR. apply between_exchange4 with x1; Between. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Highschool.triangles GeoCoq.Tarski_dev.Ch12_parallel