proposition: Lemma sum3_to_sum4 : forall O E E' A B C X ABC S , sum3 O E E' A B C ABC -> Sum O E E' ABC X S -> Sum4 O E E' A B C X S.
proof: Proof. intros. assert(~Col O E E' /\ Col O E A /\ Col O E B /\ Col O E C /\ Col O E ABC). apply sum3_col; auto. assert(Ar2 O E E' ABC X S). apply sum_ar2; auto. unfold Ar2 in H2. spliter. clean_duplicated_hyps. unfold Sum4. exists ABC. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg