proposition: Lemma sum4_equiv : forall O E E' A B C D S, Sum4 O E E' A B C D S <-> sum22 O E E' A B C D S.
proof: Proof. intros. split. intro. assert(~Col O E E' /\ Col O E A /\ Col O E B /\ Col O E C /\ Col O E D /\ Col O E S). apply sum4_col; auto. spliter. assert(HS1:= sum_exists O E E' H0 A B H1 H2). assert(HS2:= sum_exists O E E' H0 C D H3 H4). ex_and HS1 AB. ex_and HS2 CD. unfold sum22. exists AB. exists CD. assert(Ar2 O E E' A B AB). apply sum_ar2; auto. assert(Ar2 O E E' C D CD). apply sum_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. split; auto. split; auto. unfold Sum4 in H. ex_and H ABC. unfold sum3 in H. ex_and H AB'. assert(AB' = AB). apply(sum_uniqueness O E E' A B); auto. subst AB'. assert(HH:= sum_assoc O E E' AB C D ABC CD S H9 H7). destruct HH. apply H11. assumption. intro. unfold sum22 in H. ex_and H AB. ex_and H0 CD. assert(Ar2 O E E' A B AB). apply sum_ar2; auto. assert(Ar2 O E E' C D CD). apply sum_ar2; auto. assert(Ar2 O E E' AB CD S). apply sum_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. unfold Sum4. assert(HS:=sum_exists O E E' H2 AB C H13 H8). ex_and HS ABC. exists ABC. split. unfold sum3. exists AB. split; auto. assert(HH:= sum_assoc O E E' AB C D ABC CD S H3 H0). destruct HH. apply H4. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg