proposition: Lemma isosceles_foot__midpoint_conga : forall H, isosceles A B C -> Col H A C -> Perp H B A C -> ~ Col A B C /\ A<>H /\ C<>H /\ Midpoint H A C /\ CongA H B A H B C.
proof: Proof. intros. assert_diffs. assert (~ Col A B C). { intro;apply perp_not_col2 in H2. destruct H2;apply H2;ColR. } assert_diffs. assert (A<>H). { intro. treat_equalities. assert (Lt A B B C /\ Lt A C B C). apply (l11_46 B A C);Col; left;apply perp_per_2;auto. spliter. unfold isosceles in *. apply (cong__nlt A B B C);auto. } assert (C<>H). { intro. treat_equalities. assert (Lt C B B A /\ Lt C A B A). apply (l11_46 B C A);Col; left;apply perp_per_2;finish. spliter. unfold isosceles in *. apply (cong__nlt C B B A);finish. } assert (Perp_at H A C B H) by (apply l8_14_2_1b_bis;finish). assert (Per A H B) by (apply perp_in_per_1 with C H;finish). assert (Per C H B) by (apply perp_in_per_3 with A H;finish). assert (Cong H A H C /\ CongA H A B H C B /\ CongA H B A H B C) by (apply (cong2_per2__cong_conga2 A H B C H B);finish). spliter. assert (Midpoint H A C) by (apply l7_20_bis;finish). auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.perp_bisect