proposition: Lemma sum_diff2_diff_sum2_a : forall O E E' A B C X Y Z dXA dYB dZC, Sum O E E' A B C -> Sum O E E' X Y Z -> Diff O E E' X A dXA -> Diff O E E' Y B dYB -> Sum O E E' dXA dYB dZC -> Diff O E E' Z C dZC.
proof: Proof. intros. assert(Ar2 O E E' A B C). apply sum_ar2; auto. assert(Ar2 O E E' X Y Z). apply sum_ar2; auto. assert(Ar2 O E E' dXA dYB dZC). apply sum_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. apply diff_sum in H1. apply diff_sum in H2. apply sum_diff. assert(HH:=sum_exists O E E' H4 C dZC H15 H9); auto. ex_and HH Z'. assert(sum22 O E E' A B dXA dYB Z'). unfold sum22. exists C. exists dZC. auto. apply sum22_comm in H6. apply sum22_permut in H6. apply sum22_comm in H6. unfold sum22 in H6. ex_and H6 Y'. ex_and H16 X'. assert(X' = X). apply(sum_uniqueness O E E' A dXA); auto. subst X'. assert(Y'=Y). apply(sum_uniqueness O E E' B dYB); auto. subst Y'. assert( Z'= Z). apply(sum_uniqueness O E E' X Y); auto. apply sum_comm; auto. subst Z'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg