proposition: Lemma bisector_perp_equality : forall A B C I H1 H2, Coplanar A B C I -> Col B H1 A -> Col B H2 C -> Perp A B I H1 -> Perp B C I H2 -> CongA A B I I B C -> Cong I H1 I H2.
proof: Proof. intros A B C I H1 H2 HCOP HCABH HCCBH HPH1 HPH2 HCONGA. destruct (col_dec A B C) as [HCOL | HNCOL]. assert (Perp A B I H2) by (assert_diffs;apply (perp_col2 B C A B I H2);Col). assert (H1 = H2). { apply (l8_14_2_1b H1 A B I H1 H2);auto. apply (l8_14_2_1b_bis A B I H1 H1);Col. ColR. assert (Perp I H1 A B) by Perp. assert (Perp I H2 A B) by Perp. assert (Col I H1 H2) by (apply (cop_perp2__col I H1 H2 A B); Cop). Col. } subst;Cong. destruct (not_col_bfoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];auto. Col. Col. destruct (out_dec B H1 A) as [HOUT | HNOUT]. assert (Out B H2 C) by (apply (bisector_foot_out_out A B C I H1 H2);Col). apply (l11_50_2 I B H1 I B H2). { intro. elim HNCOL. col_with_conga. } { assert_diffs. apply (l11_16 B H1 I B H2 I);auto. apply (perp_per_1 H1 B I). apply (perp_col2 A B H1 B I H1);Col. assert (Perp B H2 I H2) by (apply (perp_col B C I H2 H2);Col). apply (perp_per_1 H2 B I);Perp. } assert (CongA H1 B I I B H2). { assert_diffs. apply (l11_10 A B I I B C H1 I I H2);Out. } CongA. Cong. destruct (symmetric_point_construction A B) as [A' HCONHA']. destruct (symmetric_point_construction C B) as [C' HCONHC']. assert (Bet A B A') by (apply (midpoint_bet A B A');auto). assert (Bet C B C') by (apply (midpoint_bet C B C');auto). assert (Out B H1 A'). { assert (Bet A B H1). apply (not_out_bet A B H1);auto. Col. intro. elim HNOUT. apply (l6_6 B A H1);auto. apply (l6_3_2 H1 A' B);auto. assert_diffs. repeat split;auto. exists A. repeat split;Between. } assert (Out B H2 C'). { assert_diffs. apply (bisector_foot_out_out A' B C' I H1 H2);auto. intro. elim HNCOL. ColR. CopR. ColR. apply (conga_right_comm A' B I C' B I);auto. apply (l11_13 A B I C B I A' C');CongA. apply (perp_col2 A B A' B I H1);Col. apply (perp_col2 B C B C' I H2);Col. } apply (l11_50_2 I B H1 I B H2). { intro;elim HNCOL. col_with_conga. } assert (Per B H1 I). { apply (perp_per_1 H1 B I). apply (perp_col2 A B H1 B I H1);Col. } assert (Per B H2 I) by (apply (perp_per_1 H2 B I); assert (Perp B H2 I H2) by (apply (perp_col B C I H2 H2);Col);Perp). assert_diffs. apply (l11_16 B H1 I B H2 I);auto. assert (CongA H1 B I I B H2). { assert_diffs. apply (l11_10 A' B I I B C' H1 I I H2);Out. assert (CongA A' B I C' B I) by (apply (l11_13 A B I C B I A' C');CongA). CongA. } CongA. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Highschool.triangles GeoCoq.Tarski_dev.Ch12_parallel