proposition: Lemma Qlt_floor_alt (x : Q) : x - 1 < inject_Z (Qfloor x).
proof: Proof. apply Qplus_lt_l with 1. ring_simplify. change 1 with (inject_Z 1). rewrite <-inject_Z_plus. apply Qlt_floor. 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