proposition: Lemma absℚ_realizer : forall e, absℚ↓e ⊩ ∀₁q∈ℚ, ℚ (Qcabs q).
proof: Proof. Kmove. apply Qq_realizer. exists ([q] → (0<=q ↦ ℚ (Qcabs q)) → (~0<=q ↦ ℚ (Qcabs q)) → ℚ (Qcabs q)). find. start. destruct (Qclt_le_dec q 0); Ksolve. now apply Qclt_not_le. start. apply mℚ_storage. findn 3. now rewrite Qcabs_pos in Hπ. start. apply ℚopp_realizer. findn 3. rewrite Qcabs_neg in Hπ. ok. apply Qclt_le_weak. now apply Qcnot_le_lt. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase