proposition: Lemma dedekind__cantor : dedekind_s_axiom -> cantor_s_axiom.
proof: Proof. intros dedekind A B HAB. assert (HX : exists X, forall An Bm, (exists n, 0 < n /\ A n An) -> (exists m, B m Bm) -> Bet An X Bm). - apply dedekind. destruct (nested__ex_left A B 0 HAB) as [A0]. exists A0. intros An Bm [n [Hn HAn]] [m HBm]. apply (nested__bet A B 0 n m); assumption. - destruct HX as [X HX]. exists X. intros n An Bn HAn HBn. destruct (Nat.eq_0_gt_0_cases n); [|apply HX; exists n; auto]. subst. destruct (nested__ex_left A B 1 HAB) as [A1]. apply between_exchange2 with A1. apply (nested_aux2 A B 0 1); auto. apply HX; [exists 1; split| exists 0]; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Ch07_midpoint Arith