proposition: Lemma l12_20_bis : forall A B C D, Par A B C D -> Cong A B C D -> TS B D A C -> Par B C D A /\ Cong B C D A /\ TS A C B D.
proof: Proof. intros. assert(B <> C) by (assert_diffs; auto). assert(A <> D) by (assert_diffs; auto). assert(~ Col A B C). intro. assert(Col A B D). apply not_strict_par1 with C C; Col; Par. unfold TS in H1. spliter. contradiction. assert(exists P, Midpoint P A C) by (apply midpoint_existence). ex_and H5 P. double B P D'. assert(Par B C D' A). eapply l12_17. assumption. apply H5. apply l7_2. assumption. assert(Par A B C D'). assert_diffs; apply l12_17 with P; auto. assert(Cong C D' A B). apply (l7_13 P); assumption. assert(Cong B C D' A). apply (l7_13 P); Midpoint. assert(Par C D C D'). eapply par_trans. apply par_symmetry. apply H. assumption. assert(Col C D D'). apply par_id; assumption. assert(Cong C D C D'). apply (cong_transitivity _ _ A B); Cong. assert(D = D' \/ Midpoint C D D'). apply l7_20; Col. induction H14. { subst D'. assert(Par B C D A) by Par. split. assumption. assert(HH:=l12_19 A B C D H4 H H14). spliter. split; assumption. } exfalso. assert(TS A C B D). apply par_two_sides_two_sides; assumption. assert(~ Col A C D). apply (par_not_col A B C D A); Col. apply par_not_col_strict with C; Col. assert(~ Col D' A C). intro. apply H16. ColR. assert(TS A C B D'). repeat split; Col. exists P. split. Col. Between. assert (TS A C D D'). repeat split; Col. exists C. split. Col. Between. apply (l9_9 A C B D). assumption. apply l9_8_1 with D'; assumption. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID