proposition: Lemma sum22_permut : forall O E E' A B C D S, sum22 O E E' A B C D S -> sum22 O E E' D A B C S.
proof: Proof. intros. assert(HH:= sum4_equiv O E E' A B C D S). destruct HH. assert(Sum4 O E E' A B C D S). apply H1; auto. assert(Sum4 O E E' D A B C S). apply sum4_permut; auto. assert(HH:= sum4_equiv O E E' D A B C S). destruct HH. apply H4. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg