proposition: Lemma space_separation_implies_median_planes : space_separation_axiom -> median_planes_axiom.
proof: Proof. intro sep. apply median_planes_aux. intros A B. assert (Haux : forall X P Q M, P <> Q -> Cong A P A Q -> Cong B P B Q -> Midpoint M P Q -> TSP M A B Q X -> Cong X P X Q -> False). { intros X P Q M HPQ HA HB HM [HQ [HX [T [HT HBet]]]]. assert (HCong : forall C, Coplanar M A B C -> Cong C P C Q). intros; apply (l11_60_aux M A B); Cong; apply ncop__ncol with Q, HQ. apply triangle_strict_inequality with T; Between. intro. apply (not_bet_and_out P M Q); split; [Between|]. assert (~ Coplanar M A B P) by (intro HP; apply HCong in HP; treat_equalities; auto). assert_diffs. assert (forall Z, ~ Coplanar M A B Z -> Z <> T) by (intros Z HZ He; subst; apply HZ, HT). assert (X <> T) by auto. replace M with T. apply l6_2 with X; Between. apply (col2_cop2__eq M A B P Q); Cop; ColR. } intros C P Q M HPQ HA HB HC HM. destruct (cop_dec M A B C) as [HCop|HNCop]; [apply HCop|]. assert (~ Col M A B) by (apply ncop__ncol with C, HNCop). assert (HQ : ~ Coplanar M A B Q). intro Ha; apply (l11_60_aux _ _ _ _ P Q) in Ha; Cong; treat_equalities; auto. exfalso. destruct (sep M A B Q C HQ HNCop). eauto. apply l7_2 in HM. apply (Haux C Q P M); Cong. apply l9_38, l9_41_2 with Q; [|assumption]. repeat split; trivial. intro Ha; apply (l11_60_aux _ _ _ _ P Q) in Ha; Cong; treat_equalities; auto. exists M; split; Between; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv