proposition: Lemma sum_A_O : forall A, Col O E A -> Sum O E E' A O A.
proof: Proof. intros. unfold Sum. split. repeat split; Col. assert(O <> E' /\ E <> E'). split; intro; subst E'; apply grid_ok; Col. spliter. induction (eq_dec_points A O). exists O. exists O. repeat split; Col; unfold Pj ; try auto. assert(~ Par E E' O E'). intro. induction H3. apply H3. exists E'. split; Col. spliter. apply grid_ok. Col. assert(HH:= project_existence A O E' E E' H1 H0 H3). ex_and HH A'. unfold unique in H4. spliter. exists A'. exists A'. unfold Proj in H4. spliter. repeat split; Col. unfold Pj. induction H9. left. apply par_symmetry. Par. tauto. unfold Pj. tauto. unfold Pj. left. right. repeat split; Col. intro. subst A'. induction H9. induction H9. apply H9. exists E. split; Col. spliter. contradiction. contradiction. unfold Pj. induction H9. left. apply par_symmetry. Par. right. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg