proposition: Lemma cantor__cantor_variant : FunctionalChoice_on nat Tpoint -> cantor_s_axiom <-> cantor_variant.
proof: Proof. intro choice. split. intros cantor A B HAB; apply cantor, nested_bis__nested, HAB. intros cantor A B [H1 H2]. destruct (choice A) as [fA HfA]. intro n; destruct (H1 n) as [An [_ [HAn _]]]; exists An; exact HAn. destruct (choice B) as [fB HfB]. intro n; destruct (H1 n) as [_ [Bn [_ HBn]]]; exists Bn; exact HBn. assert (HN : Nested_bis (fun n => (fun An => An = fA n)) (fun n => (fun Bn => Bn = fB n))). { split; [|split; [|split]]; intro n. - exists (fA n), (fB n); split; apply eq_refl. - intros; subst; apply eq_refl. - intros; subst; apply eq_refl. - intros An Am Bm Bn; intros; subst. apply (H2 n); auto. } apply cantor in HN. destruct HN as [X HX]. exists X. intros n An Bn HAn HBn. destruct (H2 n An (fA (S n)) (fB (S n)) Bn) as [HBet1 [HBet2 Hd]]; auto. assert (HBet3 : Bet (fA (S n)) X (fB (S n))) by (apply (HX (S n)); apply eq_refl). clear dependent A; clear dependent B. apply bet3__bet with (fA (S n)) (fB (S n)); eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le GeoCoq.Axioms.continuity_axioms Logic.ChoiceFacts