proposition: Lemma sum_uniquenessB : forall A X Y C, Sum O E E' A X C -> Sum O E E' A Y C -> X = Y.
proof: Proof. intros. induction (eq_dec_points A O). subst A. assert(X = C). apply(sum_O_B_eq X C H). assert(Y = C). apply(sum_O_B_eq Y C H0). subst X. subst Y. auto. assert(HSx:= H). assert(HSy:= H0). unfold Sum in H. unfold Sum in H0. spliter. assert(Hx:=H). assert(Hy:=H0). unfold Ar2 in H. unfold Ar2 in H0. spliter. ex_and H2 A''. ex_and H10 C''. ex_and H3 A'. ex_and H14 C'. clean_duplicated_hyps. assert(A' <> O /\ (Par_strict O E A' C' \/ X = O)). apply(sum_par_strict A X C A' C'); auto. assert(A'' <> O /\ (Par_strict O E A'' C'' \/ Y = O)). apply(sum_par_strict A Y C A'' C''); auto. spliter. unfold Pj in *. induction(eq_dec_points X O). subst X. assert(HH:=sum_A_O A H7). assert(C = A). apply (sum_uniqueness A O); auto. subst C. assert(Y=O). apply (sum_A_B_A A ); auto. subst Y. auto. induction H2. induction H3. assert(Par A A' A A''). apply (par_trans _ _ E E'); Par. induction H19. apply False_ind. apply H19. exists A. split; Col. spliter. assert(A' = A''). apply (l6_21 O E' A A'); Col. intro. apply grid_ok. apply(col_transitivity_1 _ A); Col. subst A''. induction H4. induction H6. assert(Par A' C' A' C''). apply(par_trans _ _ O E); left; Par. induction H23. apply False_ind. apply H23. exists A'. split; Col. spliter. induction H13. induction H17. assert(Par C C' C C''). apply(par_trans _ _ E' E); Par. induction H27. apply False_ind. apply H27. exists C. split; Col. spliter. assert(C' = C''). apply (l6_21 A' C' C C'); Col. intro. apply H6. exists C. split; Col. subst C''. clean_trivial_hyps. induction H12. induction H16. assert(Par Y C' X C'). apply (par_trans _ _ O E'); Par. induction H21. apply False_ind. apply H21. exists C'. split; Col. spliter. apply(l6_21 O E C' X); Col. intro. apply H4. exists C'. split; Col. subst X. clean_duplicated_hyps. apply False_ind. apply H6. exists C'. split; Col. subst Y. apply False_ind. apply H6. exists C'. split; Col. subst C'. clean_duplicated_hyps. clean_trivial_hyps. apply False_ind. apply H6. exists C. split; Col. subst C''. apply False_ind. apply H4. exists C. split; Col. subst X. tauto. subst Y. assert(A = C). apply(sum_A_O_eq A C HSy). subst C. clean_duplicated_hyps. clean_trivial_hyps. apply(sum_A_B_A A); auto. subst A'. clean_duplicated_hyps. induction H15. induction H6. apply False_ind. apply H3. exists A. split; Col. subst X. tauto. subst C'. induction H6. apply False_ind. apply H. exists A. split; Col. contradiction. subst A''. induction H4. apply False_ind. apply H2. exists A. split; Col. subst Y. assert(A = C). apply (sum_A_O_eq A C HSy). subst C. apply (sum_A_B_A A _ HSx). Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg