proposition: Lemma Qlt_Qceiling (q : Q) : inject_Z (Qceiling q) < q + 1.
proof: Proof. apply Qplus_lt_l with (z := (-1 # 1)). setoid_replace (q + 1 + (-1 # 1))%Q with q. + assert (A := Qceiling_lt q). unfold Z.sub in A. now rewrite inject_Z_plus, inject_Z_opp in A. + now rewrite <- Qplus_assoc, Qplus_opp_r, Qplus_0_r. 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