proposition: Lemma sum_diff_diff_a : forall O E E' A B C dBA dCB dCA, Diff O E E' B A dBA -> Diff O E E' C B dCB -> Diff O E E' C A dCA -> Sum O E E' dCB dBA dCA.
proof: Proof. intros. assert(Ar2 O E E' B A dBA). apply diff_ar2; auto. assert(Ar2 O E E' C B dCB). apply diff_ar2; auto. assert(Ar2 O E E' C A dCA). apply diff_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. unfold Diff in H. ex_and H mA. unfold Diff in H0. ex_and H0 mB. unfold Diff in H1. ex_and H1 mA'. assert(mA' = mA). apply (opp_uniqueness O E E' H2 A); auto. subst mA'. assert(HH:=sum_exists O E E' H2 dBA dCB H13 H10). ex_and HH Sd. assert(sum22 O E E' B mA C mB Sd). unfold sum22. exists dBA. exists dCB. split; auto. apply sum22_permut in H9. unfold sum22 in H9. ex_and H9 O'. ex_and H14 dCA'. assert(O' = O). apply (sum_uniqueness O E E' mB B); auto. subst O'. assert(dCA'=dCA). apply (sum_uniqueness O E E' C mA); auto. apply sum_comm; auto. subst dCA'. assert(dCA=Sd). apply (sum_O_B_eq O E E'); auto. subst Sd. apply sum_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg