proposition: Lemma sum_to_sump : forall O E E' A B C, Sum O E E' A B C -> Sump O E E' A B C.
proof: Proof. intros. unfold Sum in H. unfold Ar2 in H. spliter. repeat split; Col. ex_and H0 A'. ex_and H4 C'. exists A'. exists C'. assert(O <> E /\ O <> E'). repeat split; intro; subst O; apply H; Col. spliter. assert(HH:=parallel_existence1 O E A' H8). ex_and HH P'. exists P'. assert( E <> E'). intro. subst E'. apply H. Col. repeat split; Col. intro. induction H12. apply H12. exists E'. split; Col. spliter. contradiction. unfold Pj in H0. induction H0. left. apply par_symmetry. assumption. right. auto. apply par_distincts in H10. spliter. auto. intro. assert(Par O E O E'). apply (par_trans _ _ A' P'); auto. induction H13. apply H13. exists O. split; Col. spliter. apply H. Col. unfold Pj in H5. induction H5. assert(Par A' C' A' P'). apply (par_trans _ _ O E). apply par_symmetry. auto. auto. induction H12. apply False_ind. apply H12. exists A'. split; Col. spliter. Col. subst C'. Col. unfold Pj in H6. induction H6. left. apply par_symmetry. auto. right. auto. intro. induction H12. apply H12. exists E. split; Col. spliter. contradiction. unfold Pj in H7. induction H7. left. apply par_symmetry. apply par_left_comm. auto. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg