proposition: Lemma sum_diff_diff_b : forall O E E' A B C dBA dCB dCA, Diff O E E' B A dBA -> Diff O E E' C B dCB -> Sum O E E' dCB dBA dCA -> Diff O E E' C A 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' dCB dBA dCA). apply sum_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. assert(sum22 O E E' B mA C mB dCA). unfold sum22. exists dBA. exists dCB. split; auto. split; auto. apply sum_comm; auto. apply sum22_permut in H5. unfold sum22 in H5. ex_and H5 O'. ex_and H6 dCA'. assert(O'=O). apply (sum_uniqueness O E E' mB B); auto. subst O'. assert(dCA' = dCA). apply(sum_O_B_eq O E E'); auto. subst dCA'. unfold Diff. exists mA. split; auto. apply sum_comm; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg