proposition: Lemma cong_perp_conga : forall A B C P, Cong A B C B -> Perp A C B P -> CongA A B P C B P /\ TS B P A C.
proof: Proof. intros. assert(A <> C /\ B <> P). split. apply perp_not_eq_1 in H0. assumption. apply perp_not_eq_2 in H0. assumption. spliter. assert(A <> B). intro. subst B. apply cong_symmetry in H. apply cong_identity in H. apply H1. auto. assert(C <> B). intro. subst B. apply cong_identity in H. contradiction. induction(col_dec A B C). assert(~ Col B A P). apply perp_not_col. apply perp_comm. apply (perp_col _ C); Col. assert(Per P B A). apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. eapply (perp_col _ C); Col. assert(Per P B C). apply perp_in_per. apply perp_in_comm. apply perp_perp_in. apply perp_sym. eapply (perp_col _ A); Col. Perp. apply l8_2 in H7. apply l8_2 in H8. split. apply l11_16; auto. assert( A = C \/ Midpoint B A C). eapply l7_20; Cong. induction H9. contradiction. unfold TS. repeat split. auto. intro. apply H6. Col. intro. apply H6. ColR. exists B. unfold Midpoint in H9. spliter. split; [Col|Between]. assert(HH:= H0). unfold Perp in HH. ex_and HH T. apply perp_in_col in H6. spliter. assert(B <> T). intro. subst T. apply H5. Col. assert(Perp B T A C). apply (perp_col _ P); Perp. assert(A <> T). intro. subst T. apply perp_comm in H9. apply perp_perp_in in H9. apply perp_in_comm in H9. apply perp_in_per in H9. assert(Lt B A B C /\ Lt C A B C). apply( per_lt B A C); auto. spliter. unfold Lt in H10. spliter. apply H12. Cong. assert(C <> T). intro. subst T. apply perp_left_comm in H9. apply perp_perp_in in H9. apply perp_in_comm in H9. apply perp_in_per in H9. assert(Lt B C B A /\ Lt A C B A). apply( per_lt B C A); auto. spliter. unfold Lt in H11. spliter. apply H13. Cong. assert(Perp_at T B T T A). apply perp_in_comm. apply perp_perp_in. apply perp_sym. apply (perp_col _ C). assumption. apply perp_sym. apply perp_left_comm. apply (perp_col _ P); Perp. Col. assert(Perp_at T B T T C). apply perp_in_comm. apply perp_perp_in. apply perp_sym. apply (perp_col _ A). assumption. apply perp_sym. apply perp_left_comm. apply (perp_col _ P); Perp. Col. assert(Cong T A T C /\ CongA T A B T C B /\ CongA T B A T B C). apply( l11_52 A T B C T B); Cong. eapply l11_16; auto. apply perp_in_per. apply perp_in_comm. apply perp_in_sym. assumption. apply perp_in_per. apply perp_in_comm. apply perp_in_sym. assumption. assert(Lt B T B A /\ Lt A T B A). apply( per_lt B T A); auto. apply perp_in_per. assumption. spliter. apply le_comm. unfold Lt in H14. spliter. assumption. spliter. split. induction(bet_dec P B T). apply conga_comm. eapply l11_13; auto. apply H16. Between. Between. apply conga_comm. assert(Out B T P). unfold Out. repeat split; auto. induction H7. right. assumption. induction H7. left. Between. apply between_symmetry in H7. contradiction. eapply l11_10. apply H16. apply l6_6. assumption. apply out_trivial. auto. apply l6_6. assumption. apply out_trivial. auto. assert(A = C \/ Midpoint T A C). apply l7_20; Col. induction H17. contradiction. unfold TS. repeat split; Col. assert(~ Col T A B). apply perp_not_col. apply perp_in_perp_bis in H12. induction H12. apply perp_not_eq_1 in H12. tauto. Perp. intro. apply H18. ColR. assert(~ Col T C B). apply perp_not_col. apply perp_in_perp_bis in H13. induction H13. apply perp_not_eq_1 in H13. tauto. Perp. intro. apply H18. ColR. exists T. apply midpoint_bet in H17. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel