proposition: Lemma dedekind__fod : dedekind_s_axiom -> first_order_dedekind.
proof: Proof. intros dedekind Alpha Beta HAlpha HBeta HA. apply dedekind, HA. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Tarski_dev.Definitions Logic.ChoiceFacts