proposition: Lemma sum3_comm_1_2 : forall O E E' A B C S, sum3 O E E' A B C S -> sum3 O E E' B A C S.
proof: Proof. intros. assert(~Col O E E' /\ Col O E A /\ Col O E B /\ Col O E C /\ Col O E S). apply sum3_col; auto. spliter. unfold sum3 in H. ex_and H AB. unfold sum3. exists AB. split. apply sum_comm; auto. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg