proposition: Lemma cantor__completeness : (archimedes_axiom \/ ~ archimedes_axiom) -> cantor_s_axiom -> line_completeness.
proof: Proof. intros [archi|anarchy] cantor. apply dedekind_variant__completeness, (archimedes_cantor__dedekind_variant archi cantor). apply (not_archimedes__line_completeness anarchy). Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.completeness GeoCoq.Meta_theory.Continuity.dedekind_completeness GeoCoq.Meta_theory.Continuity.archimedes_cantor_dedekind