proposition: Lemma perp_equality_bisector : forall A B C I H1 H2, ~ Col A B C -> InAngle I A B C -> Col B H1 A -> Col B H2 C -> Perp A B I H1 -> Perp B C I H2 -> Cong I H1 I H2 -> CongA A B I I B C.
proof: Proof. intros A B C I H1 H2 HNCOL HINANGLE HCOLH1 HCOLH2 HPERPH1 HPERPH2 HCONG. destruct (not_col_efoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];auto. Cop. Col. Col. assert(HMY : Cong H1 B H2 B /\ CongA H1 B I H2 B I /\ CongA H1 I B H2 I B). apply (l11_52 B H1 I B H2 I). { assert_diffs. apply (l11_16 B H1 I B H2 I); auto. apply (perp_per_1 H1 B I). assert (Perp B H1 I H1) by (apply (perp_col B A I H1 H1);Perp;Col). Perp. apply (perp_per_1 H2 B I). assert (Perp B H2 I H2) by (apply (perp_col B C I H2 H2);Perp;Col). Perp. } Cong. Cong. { assert_diffs. apply (l11_46 B H1 I); auto. left. apply (perp_per_1 H1 B I). assert (Perp B H1 I H1) by (apply (perp_col B A I H1 H1);Perp;Col). Perp. } destruct HMY as [HSH1BH2B [HAH1BI HAH1IB]]. destruct (out_dec B A H1) as [HOUT | HBET]. assert (Out B H2 C) by (apply (equality_foot_out_out A B C I H1 H2);Col;apply (l6_6 B A H1);auto). assert (CongA A B I C B I). { assert_diffs. apply (l11_10 H1 B I H2 B I A I C I);Out. } CongA. assert (~ Out B C H2). { intro. assert (Out B H1 A). { apply (equality_foot_out_out C B A I H2 H1);auto. intro. elim HNCOL;Col. apply (l11_24 I A B C);auto. Col. Col. Cong. Perp. Perp. apply (l6_6 B C H2);auto. } elim HBET. apply (l6_6 B H1 A);auto. } assert (Bet A B H1) by (apply (not_out_bet A B H1);auto;Col). assert (Bet C B H2) by (apply (not_out_bet C B H2);auto;Col). assert_diffs. assert (CongA A B I C B I) by (apply (l11_13 H1 B I H2 B I A C);Between). CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Highschool.triangles GeoCoq.Tarski_dev.Ch12_parallel