proposition: Lemma not_col_bfoot_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 -> CongA A B I I B C-> 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 HCOL1 HCOL2 HCONGA HORTHA HORTHC. split. intro. subst. assert (Per A B I) by (apply (perp_per_1 B A I);Perp). assert (Col A C B). { apply cop_per2__col with I;Cop. assert_diffs;auto. apply (l8_2 I B C);auto. apply (l11_17 A B I I B C);auto. } elim HNCOL;Col. intro;subst. assert (Per C B I) by (apply (perp_per_1 B C I);auto). assert (Per I B C) by (apply (l8_2 C B I);auto). assert (Col A C B). { apply cop_per2__col with I;Cop. assert_diffs; auto. apply (l11_17 I B C A B I);CongA. } elim HNCOL; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 GeoCoq.Highschool.triangles GeoCoq.Tarski_dev.Ch12_parallel