proposition: Lemma sum_abcd : forall O E E' A B C D AB CD BC AD S, Sum O E E' A B AB -> Sum O E E' C D CD -> Sum O E E' B C BC -> Sum O E E' A D AD -> Sum O E E' AB CD S -> Sum O E E' BC AD S.
proof: Proof. intros. 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' B C BC). apply sum_ar2;auto. assert(Ar2 O E E' A D AD). apply sum_ar2;auto. assert(Ar2 O E E' AB CD S). apply sum_ar2;auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. assert(sum22 O E E' A B C D S). unfold sum22. exists AB. exists CD. split; auto. apply sum22_permut in H5. unfold sum22 in H5. ex_and H5 AD'. ex_and H6 BC'. assert(AD' = AD). apply sum_comm in H2; auto. apply (sum_uniqueness O E E' D A); auto. subst AD'. assert(BC' = BC). apply (sum_uniqueness O E E' B C); auto. subst BC'. apply sum_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg