proposition: Lemma opp_midpoint : forall O E E' A MA, Opp O E E' A MA -> Midpoint O A MA.
proof: Proof. intros. unfold Opp in H. assert(HS:=H). unfold Sum in H. spliter. unfold Ar2 in H. spliter. induction (eq_dec_points A O). subst A. assert(HH:= sum_A_O_eq O E E' H MA O HS). subst MA. unfold Midpoint. split; Cong. apply between_trivial. assert(Parallelogram_flat O MA O A). apply(sum_cong O E E' H MA A O HS). tauto. unfold Parallelogram_flat in H5. spliter. assert(A = MA \/ Midpoint O A MA). apply(l7_20 O A MA). Col. Cong. induction H10. subst MA. tauto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg