proposition: Lemma pars_par_plg : forall A B C D, Par_strict A B C D -> Par A D B C -> Plg A B C D.
proof: Proof. intros. assert(Par_strict A D B C). apply pars_par_pars; auto. assert(Par A B C D). left. assumption. assert(A <> B /\ C <> D /\ A <> D /\ B <> C). apply par_distinct in H0. apply par_distinct in H2. spliter. auto. spliter. assert(A <> C). intro. subst C. unfold Par_strict in H. spliter. apply H7. exists A. split; Col. assert(B <> D). intro. subst D. unfold Par_strict in H. spliter. apply H8. exists B. split; Col. unfold Plg. split. left. assumption. assert(HH:=midpoint_existence A C). ex_and HH M. exists M. split. assumption. prolong B M D' B M. assert(Midpoint M B D'). unfold Midpoint. split; auto. Cong. assert(Plg A B C D'). unfold Plg. repeat split. induction H. left. assumption. exists M. split; auto. assert(Parallelogram A B C D'). apply plg_to_parallelogram. assumption. assert(HH:=plg_par A B C D' H3 H6 H14). spliter. assert(~Col C A B). intro. unfold Par_strict in H. spliter. apply H18. exists C. split; Col. assert(Col C C D /\ Col D' C D). apply (parallel_uniqueness A B C D C D' C H2). Col. assumption. Col. spliter. assert(A <> D'). intro. subst D'. unfold Par_strict in H1. spliter. apply H20. exists C. split; Col. assert(HH:=mid_par_cong A B C D' M H3 H20 H9 H12). spliter. assert(Col A A D /\ Col D' A D). apply (parallel_uniqueness B C A D A D' A). Par. Col. apply par_left_comm. Par. Col. spliter. assert(D = D'). eapply (l6_21 A D C D D D'); Col. intro. unfold Par_strict in H. spliter. apply H28. exists A. split; Col. subst D'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates