proposition: Lemma maxℚ_realizer : forall e, maxℚ↓e ⊩ ∀₂p,q∈ℚ×ℚ, ℚ (Qcmax p q).
proof: Proof. intro e. startn 6. apply ℚle_realizer. find. start. apply mℚ_storage. find. start. apply mℚ_storage. find. eapply sub_stack. eassumption. start. destruct (Qclt_le_dec q p). right. split. ok. rewrite Qc.max_l in *. ok. now apply Qclt_le_weak. left. split. ok. rewrite Qc.max_r in *; ok. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase