proposition: Theorem leℚ_tight_realizer : forall e, leℚ_tight↓e ⊩ ∀₂q₁,q₂∈ℚ×ℚ, (∀₁ε∈ℚ+*, q₁ ≤ q₂ + ε) → q₁ ≤ q₂.
proof: Proof. intro e. startn 7. apply ℚle_realizer. find. + rewrite mapsto_equiv. now apply prop_realizer1. + start. apply Qq_realizer. eexists (_ → _). find. Ksolve. apply Qclt_shift_div_l. now compute. unfold Qcminus. now rewrite <- Qclt_minus_iff. + destruct (Qclt_le_dec q₂ q₁) as [Hq | Hq]. - right. split. ok. right. split. apply Qclt_not_le. Qcunfold. field_simplify. apply Qlt_shift_div_r. now compute. simpl. field_simplify. setoid_replace (2 * q₁)%Q with (q₁ + q₁)%Q by field. apply Qplus_lt_le_compat. ok. now apply Qle_refl. now compute. apply (top_bot_sub_prop Hπ). - left. now split. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase