proposition: Lemma dedekind_equiv : dedekind_s_axiom <-> dedekind_variant.
proof: Proof. split; intros dede Alpha Beta. intros A C HA HC Hdij Hcut. apply dede. exists A. intros; apply Hcut; assumption. intros [A Hcut]. destruct (classic (Beta A)) as [|HNA]. exists A; intros X Y HX HY; assert (Bet A X A) by (apply Hcut; assumption); treat_equalities; Between. destruct (classic (exists C, Beta C)) as [[C HC]|HN]; [|exists A; intros X Y HX HY; exfalso; apply HN; exists Y; apply HY]. destruct (classic (exists P, Alpha P /\ Beta P)) as [[P []]|HNconj]. exists P; intros; apply (between_exchange3 A); auto. destruct (classic (exists X, Alpha X /\ X <> A)) as [HAlpha|HN]; [|exists A; intros X Y HX HY; destruct (eq_dec_points X A); [subst; Between|exfalso; apply HN; exists X; split; assumption]]. pose (Alpha' := fun X' => X' = A \/ exists X, Alpha X /\ Bet A X' X). pose (Beta' := fun Y' => Out A Y' C /\ ~ exists X, Alpha X /\ Bet A Y' X). cut (exists B, forall X Y, Alpha' X -> Beta' Y -> Bet X B Y). { intros [B HB]. exists B. intros X Y HX HY. apply HB. right; exists X; split; Between. clear X HX. split. destruct HAlpha as [X [HX HXA]]. apply l6_7 with X; Out. intros [X [HX HAYX]]. apply HNconj; exists Y. assert (Bet A X Y) by auto. treat_equalities; split; assumption. } apply (dede Alpha' Beta' A C). - left; reflexivity. - split. apply out_trivial; intro; subst; auto. intros [X [HX HACX]]. apply HNconj; exists C. assert (C = X) by (apply (between_equality_2 A); auto). subst; split; assumption. - intros P HP. destruct (classic (exists X : Tpoint, Alpha X /\ Bet A P X)); [left; right|right; split]; auto. - intros X' Y' HX' [HY' HN]. destruct (eq_dec_points X' A). subst; split; [Between|destruct HY'; auto]. destruct HX' as [|[X [HX HAX'X]]]; [contradiction|]. assert (HOut : Out A X' Y'). assert (Bet A X C) by (apply Hcut; assumption). assert (A <> X) by (apply bet_neq21__neq with X'; assumption). apply l6_7 with X; [|apply l6_7 with C]; Out. assert (HOut' : Out Y' A X'). apply not_bet_out; Col. intro; apply HN; exists X; split; [|apply between_exchange4 with X']; assumption. split. apply out2__bet; assumption. destruct HOut' as [_ []]; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch06_out_lines Classical