proposition: Lemma sum_A_B_A : forall A B, Sum O E E' A B A -> B = O.
proof: Proof. intros. unfold Sum in H. spliter. ex_and H0 A'. ex_and H1 C'. assert(HH:= grid_not_par). spliter. induction(eq_dec_points A O). subst A. unfold Pj in *. unfold Ar2 in H. spliter. induction H0. induction H0. apply False_ind. apply H0. exists E'. split; Col. spliter. apply False_ind. apply grid_ok. ColR. subst A'. induction H2. induction H4. apply False_ind. apply H5. apply (par_trans _ _ O C') ; Par. subst C'. apply par_distincts in H0. tauto. subst C'. induction H3. induction H0. apply False_ind. apply H0. exists O. split; Col. spliter. induction(eq_dec_points B O). auto. apply False_ind. apply grid_ok. ColR. assumption. assert(A' <> O /\ (Par_strict O E A' C' \/ B = O)). apply(sum_par_strict A B A A' C');auto. spliter. induction(eq_dec_points B O). auto. induction H13. unfold Pj in *. unfold Ar2 in H. spliter. induction H0. induction H4. assert(Par A A' A C'). apply (par_trans _ _ E E'); Par. apply False_ind. induction H18. apply H18. exists A. split; Col. spliter. apply H13. exists A. split; Col. subst C'. apply False_ind. apply H13. exists A. split; Col. subst A'. apply False_ind. apply grid_ok. apply(col_transitivity_1 _ A);Col. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg