proposition: Lemma bisector_foot_out_out : forall A B C I H1 H2, ~ Col A B C -> Coplanar A B C I -> Col B C H2-> CongA A B I I B C-> Perp A B I H1 -> Perp B C I H2 -> Out B H1 A -> Out B H2 C.
proof: Proof. intros A B C I H1 H2 HNCOL HCOP HCOL2 HCONGA HORTHA HORTHC HOUT1. destruct (not_col_bfoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];Col. assert (Acute H1 B I). { apply (perp_out_acute H1 B I H1);auto. apply (out_trivial B H1);auto. apply (perp_col2 A B H1 B I H1);Col. } assert (CongA H1 B I I B C). { assert_diffs;apply (l11_10 A B I I B C H1 I I C);Out. } assert (Acute I B C) by (apply (acute_conga__acute H1 B I I B C);auto). apply (acute_col_perp__out I B C H2);auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Highschool.triangles GeoCoq.Tarski_dev.Ch12_parallel