Lemma hr_archimedean : isarchCF (λ x y : hr_ConstructiveField, hr_lt_rel y x). Proof. assert (Hadd : @isbinophrel (rigaddabmonoid NonnegativeReals) gtNonnegativeReals). { split ; intros a b c. - apply plusNonnegativeReals_ltcompat_r. - apply plusNonnegativeReals_ltcompat_l. } assert (Htra : istrans gtNonnegativeReals). { intros a b c Hab Hbc. now apply istrans_ltNonnegativeReals with b. } assert (Harch : isarchrig (@setquot_aux (rigaddabmonoid NonnegativeReals) gtNonnegativeReals)). { set (H := NonnegativeReals_Archimedean). repeat split. - intros y1 y2. apply hinhuniv. intros c. generalize (pr2 c) ; intros Hc. apply_pr2_in plusNonnegativeReals_ltcompat_l Hc. generalize (isarchrig_diff _ H _ _ Hc). apply hinhfun. intros n. exists (pr1 n). apply hinhpr. exists 0%NR. apply plusNonnegativeReals_ltcompat_l. exact (pr2 n). - intros x. generalize (isarchrig_gt _ H x). apply hinhfun. intros n. exists (pr1 n). apply hinhpr. exists 0%NR. apply plusNonnegativeReals_ltcompat_l. exact (pr2 n). - intros x. generalize (isarchrig_pos _ H x). apply hinhfun. intros n. exists (pr1 n). apply hinhpr. exists 0%NR. apply plusNonnegativeReals_ltcompat_l. exact (pr2 n). } intros x. generalize (isarchring_isarchCF (X := hr_ConstructiveField) _ (isarchrigtoring NonnegativeReals gtNonnegativeReals ispositive_oneNonnegativeReals Hadd Htra Harch) x). apply hinhfun. intros n. exists (pr1 n). generalize (pr1 n) (pr2 n) ; clear n ; intros n Hn. simpl pr1. rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij (@nattoring hr_ConstructiveField n)) in Hn |- *. revert Hn. apply hinhfun ; simpl. intros c. exact c. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.