proposition: Lemma NonnegativeReals_Archimedean : isarchrig gtNonnegativeReals.
proof: Proof. set (H := isarchNonnegativeRationals). repeat split. - intros y1 y2 Hy. generalize (NonnegativeReals_dense _ _ Hy). apply hinhuniv ; clear Hy. intros r2. generalize (NonnegativeReals_dense _ _ (pr2 (pr2 r2))). apply hinhuniv. intros r1. generalize (isarchrig_diff _ H _ _ (pr2 (NonnegativeRationals_to_NonnegativeReals_lt (pr1 r2) (pr1 r1)) (pr1 (pr2 r1)))). apply hinhfun. intros n. exists (pr1 n). eapply istrans_le_lt_ltNonnegativeReals, istrans_lt_le_ltNonnegativeReals. 2: apply NonnegativeRationals_to_NonnegativeReals_lt, (pr2 n). 1: rewrite NonnegativeRationals_to_NonnegativeReals_plus, NonnegativeRationals_to_NonnegativeReals_mult, NonnegativeRationals_to_NonnegativeReals_nattorig. 1: apply plusNonnegativeReals_lecompat_r, multNonnegativeReals_lecompat_r'. 1: apply lt_leNonnegativeReals, (pr1 (pr2 r2)). rewrite NonnegativeRationals_to_NonnegativeReals_mult, NonnegativeRationals_to_NonnegativeReals_nattorig. apply multNonnegativeReals_lecompat_r'. apply lt_leNonnegativeReals, (pr2 (pr2 r1)). - intros x. generalize (Dcuts_def_corr_finite _ (is_Dcuts_corr x)). apply hinhuniv ; intros r. generalize (isarchrig_gt _ H (pr1 r)). apply hinhfun. intros n. exists (pr1 n). apply istrans_le_lt_ltNonnegativeReals with (NonnegativeRationals_to_NonnegativeReals (pr1 r)). + apply NonnegativeRationals_to_Dcuts_notin_le. exact (pr2 r). + rewrite <- NonnegativeRationals_to_NonnegativeReals_nattorig. apply NonnegativeRationals_to_NonnegativeReals_lt. exact (pr2 n). - intros x. apply hinhpr. exists 1%nat. apply istrans_lt_le_ltNonnegativeReals with 1. + apply ispositive_oneNonnegativeReals. + apply plusNonnegativeReals_le_l. Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals