proposition: Lemma midpoint_existence : forall A B, exists X, Midpoint X A B.
proof: Proof. intros. induction (eq_dec_points A B). subst B. exists A. apply l7_3_2. cut(exists Q, Perp A B B Q). intro. ex_elim H0 Q. cut(exists P, exists T, Perp A B P A /\ Col A B T /\ Bet Q T P). intros. ex_elim H0 P. ex_and H2 T. assert (Le A P B Q \/ Le B Q A P) by (apply le_cases). induction H4. apply midpoint_existence_aux with P Q T; Perp. assert (exists X : Tpoint, Midpoint X B A) by (apply (midpoint_existence_aux B A Q P T); finish). ex_elim H5 X. exists X. Midpoint. apply l8_21;assumption. assert (exists P : Tpoint, (exists T : Tpoint, Perp B A P B /\ Col B A T /\ Bet A T P)) by (apply (l8_21 B A);auto). ex_elim H0 P. ex_elim H1 T. spliter. exists P. Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR