proposition: Lemma sum22_comm : forall O E E' A B C D S, sum22 O E E' A B C D S -> sum22 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 sum22_col; auto. spliter. unfold sum22 in H. ex_and H AB. ex_and H6 CD. unfold sum22. exists AB. exists CD. split; auto. apply sum_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg