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