proposition: Theorem Archimed : forall e, Archimedℝ↓e ⊩ ∀₁x∈ℝ, ∃₁q∈ℚ, (x <= q)%Re.
proof: Proof. intro e. start. apply Qq_realizer. find. start. apply Ht. find. now compute. find. start. apply Qq_realizer. find. start. apply ℚadd_realizer. find. find. Ksolve. find. start. apply (prop_guard Ht4). intros [_ ?]. subst. apply Qq_realizer. find. Kmove. exists ε₁, 1. find. now compute. find. apply (prop_subst_stack Hπ). clear -Hc0. rewrite Qcabs_minus, Qcabs_diff_le_condition. intros [_ ?]. rewrite <- Qcplus_0_r at 1. apply Qcplus_le_compat. rewrite <- Qcplus_assoc. now setoid_rewrite Qcplus_comm at 2. assumption. Qed.
imports: ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations ClassicalRealizability.Real_operations