proposition: Lemma archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1.
proof: Proof. intro r. unfold up. destruct (CRealArchimedean (Rrepr r)) as [n nmaj], (total_order_T (IZR n - r) R1). 1:destruct s. - split. + unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. apply CRealLtForget. apply nmaj. + unfold Rle. left. exact r0. - split. + unfold Rgt. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR. apply CRealLtForget. apply nmaj. + right. exact e. - split. + unfold Rgt, Z.pred. rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_IZR, inject_Z_plus. rewrite RbaseSymbolsImpl.Rlt_def in r0. rewrite Rrepr_minus in r0. rewrite <- (Rrepr_IZR n). apply CRealLtForget. apply CRealLtEpsilon in r0. unfold CReal_minus in r0. apply (CReal_plus_lt_compat_l (CReal_plus (Rrepr r) (CReal_opp (Rrepr R1)))) in r0. rewrite CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r, RbaseSymbolsImpl.R1_def, Rquot2, CReal_plus_comm, CReal_plus_assoc, <- (CReal_plus_assoc (CReal_opp (Rrepr r))), CReal_plus_opp_l, CReal_plus_0_l in r0. rewrite (opp_inject_Z 1). exact r0. + destruct (total_order_T (IZR (Z.pred n) - r) 1). * destruct s. -- left. exact r1. -- right. exact e. * exfalso. destruct nmaj as [_ nmaj]. pose proof Rrepr_IZR as iz. rewrite <- iz in nmaj. apply (Rlt_asym (IZR n) (r + 2)). -- rewrite RbaseSymbolsImpl.Rlt_def. rewrite Rrepr_plus. rewrite (Rrepr_plus 1 1). apply CRealLtForget. apply (CReal_lt_le_trans _ _ _ nmaj). unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, Rquot2. rewrite <- (inject_Z_plus 1 1). apply CRealLe_refl. -- clear nmaj. unfold Z.pred in r1. rewrite RbaseSymbolsImpl.Rlt_def in r1. rewrite Rrepr_minus, (Rrepr_IZR (n + -1)) in r1. rewrite inject_Z_plus, <- (Rrepr_IZR n) in r1. rewrite RbaseSymbolsImpl.Rlt_def, Rrepr_plus. apply CRealLtEpsilon in r1. apply (CReal_plus_lt_compat_l (CReal_plus (Rrepr r) 1%CReal)) in r1. apply CRealLtForget. apply (CReal_le_lt_trans _ (CReal_plus (CReal_plus (Rrepr r) (Rrepr 1)) 1%CReal)). ++ rewrite (Rrepr_plus 1 1). unfold IZR, IPR. rewrite RbaseSymbolsImpl.R1_def, (Rquot2 1%CReal), <- CReal_plus_assoc. apply CRealLe_refl. ++ rewrite <- (CReal_plus_comm (Rrepr 1)), <- CReal_plus_assoc, (CReal_plus_comm (Rrepr 1)) in r1. apply (CReal_lt_le_trans _ _ _ r1). unfold CReal_minus. rewrite (opp_inject_Z 1). rewrite (CReal_plus_comm (Rrepr (IZR n))), CReal_plus_assoc, <- (CReal_plus_assoc 1), <- (CReal_plus_assoc 1), CReal_plus_opp_r. rewrite CReal_plus_0_l, CReal_plus_comm, CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r. apply CRealLe_refl. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions