proposition: Theorem Qmin_l : ∀ n m, (n <= m)%Q → Qmin n m == n.
proof: Proof. intros n m H. unfold Qmin. destruct (Qlt_le_dec n m) as [| Hge]; [ reflexivity | idtac ]. apply Qle_antisym; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Psatz