proposition: Lemma plg_to_sum : forall O E E' A B C, Ar2 O E E' A B C ->Parallelogram_flat O A C B -> Sum O E E' A B C.
proof: Proof. intros. induction(eq_dec_points A B). subst B. unfold Parallelogram_flat in H0. spliter. assert(O = C \/ Midpoint A O C). apply(l7_20 A O C H0). Cong. induction H5. subst C. tauto. apply cong_sum; auto. unfold Ar2 in H. tauto. unfold Midpoint in H5. tauto. unfold Midpoint in H5. tauto. unfold Ar2 in H. unfold Parallelogram_flat in H0. spliter. apply cong_sum; auto. repeat split; auto. Cong. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg