proposition: Lemma l12_19 : forall A B C D , ~Col A B C -> Par A B C D -> Par B C D A -> Cong A B C D /\ Cong B C D A /\ TS B D A C /\ TS A C B D.
proof: Proof. intros. assert(exists P, Midpoint P A C) by (eapply midpoint_existence). ex_and H2 P. double B P D'. assert(Cong C D' A B). apply (l7_13 P); assumption. assert(Cong B C D' A). apply (l7_13 P); Midpoint. assert(Par A B C D'). assert_diffs; apply l12_17 with P; auto. assert(Par C D C D'). eapply par_trans. apply par_symmetry. apply H0. apply H6. assert(Col C D D'). apply par_id. assumption. assert(Par B C D' A). assert_diffs; apply l12_17 with P; Midpoint. assert(Par D A D' A). eapply par_trans. apply par_symmetry. apply H1. assumption. assert(Col A D D'). apply par_id. Par. assert(D = D'). assert_diffs; apply (l6_21 A D C D); Col. intro. apply H. assert(Col P C D). apply col_permutation_2. apply (col_transitivity_1 _ A); Col. assert(Col P C D'). apply col_permutation_2. apply (col_transitivity_1 _ D); Col. assert(Col P A D'). apply (col_transitivity_1 _ C); Col. apply (col3 P D'); Col. intro; treat_equalities; Col5. subst D'. split. Cong. split. Cong. assert(B <> D). intro; treat_equalities; Col5. split. apply l12_18_c with P; Cong; Col. apply l12_18_d with P; Cong; Col. Qed.
imports: GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID