proposition: Lemma cong_conga_perp : forall A B C P, TS B P A C -> Cong A B C B -> CongA A B P C B P -> Perp A C B P.
proof: Proof. intros. assert(HH:=H). unfold TS in HH. assert (~ Col A B P). spliter. assumption. spliter. ex_and H5 T. assert(B <> P). intro. subst P. apply H3. Col. assert(A <> B). intro. subst B. apply H3. Col. assert(C <> B). intro. subst C. apply H4. Col. assert(A <> C). intro. subst C. assert(OS B P A A). apply one_side_reflexivity. assumption. apply l9_9 in H. contradiction. induction (bet_dec A B C). assert(Per P B A). apply(l11_18_2 P B A C); auto. apply conga_comm. assumption. eapply (col_per_perp _ _ _ C) in H12; auto. apply perp_right_comm. assumption. apply bet_col in H11. Col. assert(B <> T). intro. subst T. contradiction. assert(CongA T B A T B C). induction H5. eapply (l11_13 P _ _ P); Between. apply conga_comm. apply H1. assert(Out B P T). repeat split; auto. induction H5. left. Between. right. Between. apply conga_comm. apply (l11_10 A _ P C _ P); try (apply out_trivial); auto; apply l6_6; assumption. assert(Cong T A T C). apply (cong2_conga_cong T B A T B C); Cong. assert(Midpoint T A C). split; Cong. assert(Per B T A). unfold Per. exists C. split; Cong. eapply (col_per_perp _ _ _ C) in H16; auto. apply perp_sym. apply (perp_col _ T); Col. Perp. intro. subst T. apply is_midpoint_id in H15. contradiction. intro. subst T. apply l7_2 in H15. apply is_midpoint_id in H15. apply H10. auto. apply bet_col in H6. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles