proposition: Theorem absℚ_tight_realizer : forall e, absℚ_tight↓e ⊩ ∀₂q₁,q₂∈ℚ×ℚ, (∀₁ε∈ℚ+*, |q₁| ≤ q₂ + ε) → |q₁| ≤ q₂.
proof: Proof. Ksolve. apply absℚ_realizer. find. startn 0. apply leℚ_tight_realizer. find. find. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase