proposition: Lemma diff_to_plg : forall O E E' A B dBA, A <> O \/ B <> O -> Diff O E E' B A dBA -> Parallelogram_flat O A B dBA.
proof: Proof. intros. assert(Ar2 O E E' B A dBA). apply diff_ar2; auto. unfold Ar2 in H1. spliter. apply diff_sum in H0. induction(eq_dec_points A O). subst A. assert(dBA = B). apply(sum_O_B_eq O E E'); auto. subst dBA. apply plgf_permut. apply plgf_trivial. induction H; tauto. assert(E <> O). intro. subst E. apply H1. Col. induction(eq_dec_points B O). subst B. assert(Opp O E E' dBA A). unfold Opp. auto. apply opp_midpoint in H7. unfold Midpoint in H7. spliter. unfold Parallelogram_flat. repeat split; Col. Cong. Cong. assert_diffs; auto. apply sum_cong in H0; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg