proposition: Lemma sum_uniqueness : forall A B C1 C2, Sum O E E' A B C1 -> Sum O E E' A B C2 -> C1 = C2.
proof: Proof. intros. apply sum_to_sump in H. apply sum_to_sump in H0. unfold Sump in H. unfold Sump in H0. spliter. clean_duplicated_hyps. ex_and H4 A'. ex_and H0 C'. ex_and H1 P'. ex_and H2 A''. ex_and H6 C''. ex_and H2 P''. assert(A'=A''). apply(project_uniqueness A A' A'' O E' E E');auto. subst A''. assert(Col A' P' P''). assert(Par A' P' A' P''). apply (par_trans _ _ O E). apply par_symmetry. auto. auto. induction H9. apply False_ind. apply H9. exists A'. split; Col. spliter. Col. assert(Proj B C'' A' P' O E'). eapply (project_col_project _ P''); Col. unfold Proj in H4. tauto. assert(C' = C''). apply(project_uniqueness B C' C'' A' P' O E');auto. subst C''. apply(project_uniqueness C' C1 C2 O E E E');auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg