proposition: Lemma sum4_permut: forall O E E' A B C D S, Sum4 O E E' A B C D S -> Sum4 O E E' D A B 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 D /\ Col O E S). apply sum4_col; auto. spliter. assert(HH:=sum4_equiv O E E' A B C D S). destruct HH. assert(sum22 O E E' A B C D S). apply H6; auto. unfold sum22 in H8. ex_and H8 AB. ex_and H9 CD. apply sum_comm in H9; auto. apply sum_comm in H10; auto. unfold Sum4 in H. ex_and H ABC. assert(HH:= sum_assoc O E E' D C AB CD ABC S H9). assert(HP:=sum3_permut O E E' A B C ABC H). unfold sum3 in HP. ex_and HP AC. assert(HP:= sum_assoc O E E' C A B AC AB ABC H12 H8). destruct HP. assert(Sum O E E' C AB ABC). apply H15; auto. apply HH in H16. destruct H16. assert(Sum O E E' D ABC S). apply H17; auto. assert(HP:= sum_exists O E E' H0 D A H4 H1); auto. ex_and HP AD. assert(Ar2 O E E' D A AD). apply sum_ar2; auto. unfold Ar2 in H20. spliter. clean_trivial_hyps. assert(HP:= sum_exists O E E' H0 AD B H23 H2); auto. ex_and HP ABD. assert(HP:= sum_assoc O E E' D A B AD AB ABD H19 H8). destruct HP. apply H26 in H24. unfold Sum4. exists ABD. split. unfold sum3. exists AD. split; auto. unfold sum3 in H. ex_and H AB'. assert(AB'=AB). apply (sum_uniqueness O E E' A B); auto. subst AB'. assert(HP:= sum_assoc O E E' D AB C ABD ABC S H24 H27). destruct HP. apply H28. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg