proposition: Lemma sum4_comm : forall O E E' A B C D S, Sum4 O E E' A B C D S -> Sum4 O E E' B A C D S.
proof: Proof. intros. 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(HH:= sum4_equiv O E E' A B C D S). destruct HH. apply H6 in H. unfold sum22 in H. ex_and H AB. ex_and H8 CD. apply sum_comm in H; auto. assert(sum22 O E E' B A C D S). unfold sum22. exists AB. exists CD. split; auto. assert(HH:= sum4_equiv O E E' B A C D S). destruct HH. apply H12; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg