proposition: Lemma not_col_efoot_not_equality : forall A B C I H1 H2, ~ Col A B C -> Coplanar A B C I -> Col A B H1 -> Col B C H2-> Cong I H1 I H2-> Perp A B I H1 -> Perp B C I H2 -> H1 <> B /\ H2 <> B.
proof: Proof. intros A B C I H1 H2 HNCOL HCOP HCOLH1 HCOLH2 HCONG HPERH1 HPERH2. assert (H1 <> B). intro. subst. assert (H2 <> B). { intro. subst. assert (Col B A C). apply (cop_perp2__col B A C I B);auto. Cop. Perp. elim HNCOL. Col. } assert (Perp B H2 I H2). apply (perp_col B C I H2 H2);auto. assert (Per B H2 I). { apply (perp_per_1 H2 B I);auto. Perp. } assert (Per H2 B I). { apply (l11_17 B H2 I H2 B I);auto. apply (isosceles_conga H2 I B);auto. assert_diffs;auto. unfold isosceles;Cong. } assert (H2 = B). { apply (l8_7 I H2 B);auto. apply (l8_2 B H2 I);auto. apply (l8_2 H2 B I);auto. } contradiction. split;auto. intro. subst. assert (Perp B H1 I H1) by (apply (perp_col B A I H1 H1);auto;Perp;Col). assert (Per B H1 I) by (apply (perp_per_1 H1 B I);auto;Perp). assert (Per H1 B I). { apply (l11_17 B H1 I H1 B I);auto. apply (isosceles_conga H1 I B);auto. assert_diffs;auto. unfold isosceles;Cong. } assert (H1 = B). { apply (l8_7 I H1 B);auto. apply (l8_2 B H1 I);auto. apply (l8_2 H1 B I);auto. } contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Highschool.triangles GeoCoq.Tarski_dev.Ch12_parallel