proposition: Lemma Qfloor_pos (x : Q) : 1 <= x -> (0 < Qfloor x)%Z.
proof: Proof. intros E. rewrite Zlt_Qlt. apply Qle_lt_trans with (x - 1). apply Qplus_le_l with 1. now ring_simplify. apply Qlt_floor_alt. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List