proposition: Lemma nat_lt_Qlt n m: (n < m)%nat -> (inject_Z (Z_of_nat n) + (1#2) < inject_Z (Z_of_nat m))%Q.
proof: Proof. Proof with intuition. unfold lt. intros. apply Qlt_le_trans with (inject_Z (Z_of_nat n) + 1). do 2 rewrite (Qplus_comm (inject_Z (Z_of_nat n))). apply Qplus_lt_l... pose proof (inj_le _ _ H). rewrite Zle_Qle in H0. rewrite <- S_Qplus... 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