proposition: Lemma diff_sum : forall O E E' A B S, Diff O E E' S A B -> Sum O E E' A B S.
proof: Proof. intros. assert(Ar2 O E E' S A B). apply diff_ar2; auto. unfold Ar2 in H0. spliter. induction(eq_dec_points A O). subst A. assert(HH:=diff_A_O O E E' S H0 H1). assert(S = B). apply (diff_uniqueness O E E' S O); auto. subst B. apply sum_O_B; auto. unfold Diff in H. ex_and H mA. assert(mA <> O). intro. subst mA. assert(HH:=opp0 O E E' H0). apply H4. apply (opp_uniqueness O E E' H0 O); auto. apply opp_comm; auto. unfold Opp in H. induction(eq_dec_points S O). subst S. assert(mA = B). apply (sum_O_B_eq O E E'); auto. subst mA. apply sum_comm; auto. apply sum_cong in H; auto. apply sum_cong in H5; auto. assert(E <> O). intro. subst E. apply H0. Col. assert(Parallelogram O A S B \/ O = A /\ O = mA /\ B = S /\ O = B). apply(plg_pseudo_trans O A O mA B S). apply plg_permut. apply plg_permut. right. assumption. apply plg_comm2. apply plg_permut. apply plg_permut. apply plg_permut. 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 H5. unfold Parallelogram_flat in H9. spliter. apply cong_sum; Cong. repeat split; Col. spliter. subst A. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg