proposition: Lemma equality_foot_out_out : forall A B C I H1 H2, ~ Col A B C -> InAngle I A B C -> Col B C H2 -> Cong I H1 I H2-> 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 HINANGLE HCOLH2 HCONG HPERH1 HPERH2 HOUTH1. destruct (not_col_efoot_not_equality A B C I H1 H2) as [HNEQH1 HNEQH2];Col. Cop. assert(HMY : Cong H1 B H2 B /\ CongA H1 B I H2 B I /\ CongA H1 I B H2 I B). { assert_diffs. apply (l11_52 B H1 I B H2 I);Cong. 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);auto;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);auto;Perp;Col). Perp. 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);auto;Perp;Col). Perp. } destruct HMY as [HSH1BH2B [HAH1BI HAH1IB]]. assert (TS I B A C). { apply (in_angle_two_sides A B C I);auto. intro. assert (Col H1 B H2) by (col_with_conga). elim HNCOL; ColR. intro. assert (Col H2 B H1) by (col_with_conga). elim HNCOL;ColR. } destruct (conga_cop__or_out_ts I B H1 H2) as [HOUTH1H2 | HTSH1H2]. CopR. CongA. elim HNCOL;ColR. assert (TS I B A H2) by (apply (l9_5 I B H1 H2 B A);auto;Col). assert (OS I B H2 C). { apply (l9_8_1 I B H2 C A);auto. apply (l9_2 I B A H2);auto. apply (l9_2 I B A C);auto. } apply (col_one_side_out B I H2 C). Col. apply (invert_one_side I B H2 C);auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Highschool.triangles GeoCoq.Tarski_dev.Ch12_parallel