proposition: Lemma ℚpos_ℚnoneg_subtype : forall q, ℚ+* q ⊆ ℚ+ q.
proof: Proof. unfold ℚpos. do 2 Ksolve. now apply Qclt_le_weak. Qed.
imports: QArith ClassicalRealizability.Qcabs ClassicalRealizability.Qcminmax ClassicalRealizability.Kbase