proposition: Lemma sump_to_sum : forall O E E' A B C, Sump O E E' A B C -> Sum O E E' A B C.
proof: Proof. intros. unfold Sump in H. spliter. ex_and H1 A'. ex_and H2 C'. ex_and H1 P'. unfold Sum. split. repeat split; Col. intro. unfold Proj in H1. spliter. apply H7. right. repeat split; Col. unfold Proj in H4. spliter. Col. exists A'. exists C'. unfold Pj. repeat split. unfold Proj in H1. spliter. induction H8. left. apply par_symmetry. auto. tauto. unfold Proj in H1. tauto. induction(eq_dec_points A' C'). tauto. left. unfold Proj in H3. spliter. apply (par_col_par _ _ _ P'); Col. unfold Proj in H3. spliter. induction H8. left. apply par_symmetry. auto. tauto. unfold Proj in H4. spliter. induction H8. left. apply par_symmetry. apply par_right_comm. auto. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg