proposition: Lemma sum_diff : forall O E E' A B S, Sum O E E' A B S -> Diff O E E' S A B.
proof: Proof. intros. assert(Ar2 O E E' A B S). apply sum_ar2; auto. unfold Ar2 in H0. spliter. assert(HH:=opp_exists O E E' H0 A H1). ex_and HH mA. exists mA. split; auto. unfold Opp in H4. assert(Ar2 O E E' mA A O). apply sum_ar2; auto. unfold Ar2 in H5. spliter. clean_duplicated_hyps. clear H8. induction(eq_dec_points A O). subst A. assert(B = S). apply (sum_uniqueness O E E' O B); auto. apply sum_O_B; auto. subst S. assert(mA = O). apply (sum_uniqueness O E E' mA O); auto. apply sum_A_O; auto. subst mA. apply sum_A_O; auto. induction(eq_dec_points B O). subst B. assert(A = S). apply (sum_uniqueness O E E' A O); auto. apply sum_A_O; auto. subst S. apply sum_comm; auto. apply sum_cong in H; auto. apply sum_cong in H4; auto. assert(E <> O). intro. subst E. apply H0. Col. assert(Parallelogram O mA B S \/ O = mA /\ O = A /\ S = B /\ O = S). apply(plg_pseudo_trans O mA O A S B); auto. right; auto. right; auto. induction H9. induction H9. apply False_ind. unfold Parallelogram_strict in H9. spliter. unfold TS in H9. spliter. apply H12. ColR. unfold Parallelogram_flat in H. unfold Parallelogram_flat in H4. unfold Parallelogram_flat in H9. spliter. apply cong_sum; auto. repeat split; Col. Cong. Cong. spliter. subst A. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg