proposition: Lemma sum22_col : forall O E E' A B C D S, sum22 O E E' A B C D S -> ~Col O E E' /\ Col O E A /\ Col O E B /\ Col O E C /\ Col O E D /\ Col O E S.
proof: Proof. intros. 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. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg