proposition: Lemma l13_15_par : forall A B C A' B' C', ~Col A B C -> Par_strict A B A' B' -> Par_strict A C A' C' -> Par A A' B B' -> Par A A' C C' -> Par B C B' C'.
proof: Proof. intros. assert(Plg B' A' A B). apply(pars_par_plg B' A' A B). apply par_strict_left_comm. Par. Par. apply plg_to_parallelogram in H4. apply plg_permut in H4. assert(Plg A' C' C A). apply(pars_par_plg A' C' C A). apply par_strict_right_comm. Par. Par. apply plg_to_parallelogram in H5. apply plg_permut in H5. assert(Parallelogram B B' C' C \/ B = B' /\ A' = A /\ C = C' /\ B = C). apply(plg_pseudo_trans B B' A' A C C'). apply plg_sym. auto. apply plg_comm2. apply plg_permut. apply plg_permut. auto. assert(Par B B' C C'). apply (par_trans _ _ A A'); Par. induction H7. induction H6. assert(B <> B'). apply par_distincts in H2. tauto. apply plg_par in H6. spliter. Par. auto. intro. subst C'. apply H7. exists B'. split; Col. spliter. subst C. subst C'. apply False_ind. apply H7. exists B. split; Col. induction H6. apply plg_par in H6. spliter. Par. spliter. auto. spliter. intro. subst C'. assert(Par A B A C). apply (par_trans _ _ A' B'); left; Par. induction H11. apply H11. exists A. split; Col. spliter. apply H. Col. spliter. subst B'. subst A'. subst C'. subst C. apply False_ind. apply H1. exists A. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal