proposition: Lemma Rlt_n_Sn : forall x, x < x + 1.
proof: Proof. intro. elim archimed with x; intros. destruct H0. - apply Rlt_trans with (IZR (up x)); trivial. replace (IZR (up x)) with (x + (IZR (up x) - x))%R. + apply Rplus_lt_compat_l; trivial. + unfold Rminus. rewrite (Rplus_comm (IZR (up x)) (- x)). rewrite <- Rplus_assoc. rewrite Rplus_opp_r. apply Rplus_0_l. - elim H0. unfold Rminus. rewrite (Rplus_comm (IZR (up x)) (- x)). rewrite <- Rplus_assoc. rewrite Rplus_opp_r. rewrite Rplus_0_l; trivial. Qed.
imports: Nnat ArithRing Ring Field Rdefinitions Rpow_def Raxioms