proposition: Lemma hr_archimedean : isarchCF (λ x y : hr_ConstructiveField, hr_lt_rel y x).
proof: 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.
imports: UniMath.Algebra.Groups UniMath.Foundations.Preamble UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals