proposition: Lemma sum_diff2_diff_sum2_b : 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 -> Diff O E E' Z C dZC -> Sum O E E' dXA dYB 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' X A dXA). apply diff_ar2; auto. assert(Ar2 O E E' Y B dYB). apply diff_ar2; auto. assert(Ar2 O E E' Z C dZC). apply diff_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. assert(HH:=sum_exists O E E' H4 dXA dYB H17 H14). ex_and HH dZC'. assert(HH:=sum_diff2_diff_sum2_a O E E' A B C X Y Z dXA dYB dZC' H H0 H1 H2 H5). assert( dZC' = dZC). apply(diff_uniqueness O E E' Z C); auto. subst dZC'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg