proposition: Lemma sum_uniquenessA : forall B X Y C, Sum O E E' X B C -> Sum O E E' Y B C -> X = Y.
proof: Proof. intros. induction (eq_dec_points B O). subst B. assert(X = C). apply(sum_A_O_eq X C H). subst X. assert(Y = C). apply(sum_A_O_eq Y C H0). 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. unfold Pj in *. induction(eq_dec_points X O). subst X. assert(HH:=sum_O_B B H8). assert(B = C). apply (sum_uniqueness O B); auto. subst C. apply sym_equal. apply (sum_A_B_B Y B); auto. induction(eq_dec_points Y O). subst Y. assert(HH:=sum_O_B B H8). assert(B = C). apply (sum_uniqueness O B); auto. subst C. apply (sum_A_B_B X B); auto. assert(A' <> O /\ (Par_strict O E A' C' \/ B = O)). apply(sum_par_strict X B C A' C'); auto. assert(A'' <> O /\ (Par_strict O E A'' C'' \/ B = O)). apply(sum_par_strict Y B C A'' C''); auto. spliter. induction H12. induction H16. assert(Par B C' B C''). apply (par_trans _ _ O E'); Par. induction H20. apply False_ind. apply H20. exists B. split; Col. spliter. clean_trivial_hyps. induction H13. induction H17. assert(Par C C' C C''). apply (par_trans _ _ E E'); Par. induction H22. apply False_ind. apply H22. exists C. split; Col. spliter. assert(C' = C''). apply(l6_21 C C' B C'); Col. intro. induction H19. apply H19. exists C'. split. assert(Col O B C). apply (col_transitivity_1 _ E); Col. intro. apply grid_ok. subst E. Col. assert(Col E B C). apply (col_transitivity_1 _ O); Col. intro. apply grid_ok. subst E. Col. apply(col3 B C); Col. intro. subst C. clean_trivial_hyps. apply(sum_A_B_B) in HSx. contradiction. Col. contradiction. subst C''. clean_trivial_hyps. induction H19. induction H18. assert(Par A' C' A'' C'). apply (par_trans _ _ O E);left; Par. induction H23. apply False_ind. apply H23. exists C'. split; Col. spliter. assert(A'= A''). apply (l6_21 O E' C' A'); Col. intro. induction H16. apply H16. exists C'. split; Col. spliter. apply H1. apply (l6_21 O E C' O); Col. intro. apply grid_ok. ColR. intro. subst C'. clean_trivial_hyps. apply H18. exists O. split; Col. subst A''. clean_trivial_hyps. clean_duplicated_hyps. induction H2. induction H3. assert(Par Y A' X A'). apply(par_trans _ _ E E'); Par. induction H6. apply False_ind. apply H6. exists A'. split; Col. spliter. apply (l6_21 O E A' X); Col. intro. apply H19. exists A'. split; Col. subst X. apply False_ind. apply H19. exists A'. split; Col. subst Y. apply False_ind. apply H19. exists A'. split; Col. contradiction. contradiction. subst C'. apply False_ind. induction H16. apply H16. exists O. split. Col. apply(col3 O E); Col. intro. subst E. apply grid_ok; Col. spliter. apply grid_ok. apply(colx B C); Col. subst C''. apply False_ind. induction H12. apply H12. exists O. split. Col. apply(col3 O E); Col. intro. subst E. apply grid_ok; Col. spliter. apply grid_ok. apply(colx B C); Col. apply False_ind. subst C'. induction H19. apply H16. exists B. split; Col. contradiction. subst C''. apply False_ind. induction H18. apply H12. exists B. split; Col. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg