proposition: Lemma l12_21_b : forall A B C D, TS A C B D -> CongA B A C D C A -> Par A B C D.
proof: Proof. intros. apply conga_distinct in H0. spliter. assert(~Col A B C). intro. unfold TS in H. spliter. apply col_permutation_4 in H5. assert(Col D C A). eapply col_conga_col. apply H5. assumption. contradiction. assert(A <> B /\ C <> D). auto. spliter. assert(HH:=segment_construction_3 C D A B H7 H6). ex_and HH D'. assert(CongA B A C D' C A). eapply l11_10. apply H0. apply out_trivial. assumption. apply out_trivial. assumption. apply l6_6. assumption. apply out_trivial. assumption. assert(Cong D' A B C). eapply cong2_conga_cong. apply conga_sym. apply H10. Cong. Cong. assert(TS A C D' B). eapply l9_5. apply l9_2. apply H. apply col_trivial_3. assumption. unfold TS in H12. spliter. ex_and H14 M. assert(B <> D'). intro. treat_equalities. contradiction. assert(Midpoint M A C /\ Midpoint M B D'). apply l7_21. assumption. assumption. Cong. Cong. Col. apply bet_col in H15. Col. spliter. assert(Par A B C D'). eapply l12_17. assumption. apply H17. assumption. eapply par_col_par. auto. apply H19. apply out_col in H8. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles