proposition: Lemma sum3_permut : forall O E E' A B C S, sum3 O E E' A B C S -> sum3 O E E' C A B 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. assert(HH:= sum_exists O E E' H0 A C H1 H3). ex_and HH AC. unfold sum3. exists AC. split. apply sum_comm; auto. apply sum_comm in H5; auto. apply sum_comm in H6; auto. assert(HH:=sum_assoc O E E' C A B AC AB S H6 H). destruct HH. apply H7; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg