proposition: Lemma l12_22_aux : forall A B C D P, P <> A -> A <> C -> Bet P A C -> OS P A B D -> CongA B A P D C P -> Par A B C D.
proof: Proof. intros. assert (P<>C) by (intro; treat_equalities; auto). prolong B A B' B A . spliter. assert(CongA P A B C A B'). apply l11_14. assumption. assumption. auto. assumption. unfold CongA in H3. spliter. auto. intro. treat_equalities. unfold CongA in H3. tauto. assert(CongA D C A D C P). apply out2__conga. apply out_trivial. unfold CongA in H3. tauto. apply between_symmetry in H1. apply bet_out in H1. apply l6_6. assumption. auto. assert(Par A B' C D). eapply l12_21_b. assert(~Col B P A). unfold OS in H2. ex_and H2 T. unfold TS in H2. tauto. assert(TS P A B B'). unfold TS. repeat split. assumption. intro. apply H9. apply col_permutation_1. eapply (col_transitivity_1 _ B'). intro. treat_equalities. unfold CongA in H3. tauto. apply bet_col in H1. Col. Col. exists A. split. Col. assumption. apply l9_2. apply l9_8_2 with B. apply col_two_sides with P. apply bet_col in H1. Col. assumption. apply invert_two_sides. apply H10. apply col_one_side with P. apply bet_col in H1. Col. auto. apply invert_one_side. apply H2. eapply conga_trans. apply conga_sym. apply conga_comm. apply H7. eapply conga_trans. apply H3. apply conga_sym. assumption. apply par_symmetry. apply par_col_par with B'. unfold CongA in H3. spliter. auto. apply par_symmetry. apply H9. apply bet_col in H1. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles