Library UniMath.RealNumbers.Reals

A library about decidable Real Numbers

Author: Catherine LELAY. Oct 2015 -

Require Export UniMath.Algebra.Groups.
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.
Require Export UniMath.RealNumbers.NonnegativeReals.

Local Open Scope NR_scope.

Definition

commring


Definition hr_commring : commring := commrigtocommring NonnegativeReals.

Definition NR_to_hr : NonnegativeReals × NonnegativeReals → hr_commring
  := setquotpr (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals)).

Definition nat_to_hr (n : nat) : hr_commring :=
  NR_to_hr (nat_to_NonnegativeReals n,,0).

Lemma NR_to_hr_inside :
  ∏ x : NonnegativeReals × NonnegativeReals, pr1 (NR_to_hr x) x.
Show proof.
  intros x.
  apply hinhpr ; simpl.
  exists 0 ; reflexivity.

Local Lemma iscomprelfun_NRminus :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    pr1 x + pr2 y = pr1 y + pr2 x
    → pr1 x - pr2 x = pr1 y - pr2 y.
Show proof.
  intros x y H.
  apply (plusNonnegativeReals_eqcompat_l (pr2 x)).
  rewrite <- maxNonnegativeReals_minus_plus.
  apply (plusNonnegativeReals_eqcompat_l (pr2 y)).
  rewrite isrdistr_max_plusNonnegativeReals, H.
  rewrite (iscomm_plusNonnegativeReals (pr2 x) (pr2 y)), <- isrdistr_max_plusNonnegativeReals, maxNonnegativeReals_minus_plus.
  now rewrite !isassoc_plusNonnegativeReals, (iscomm_plusNonnegativeReals (pr2 x)).

Lemma iscomprelfun_hr_to_NR :
  iscomprelfun (Y := NonnegativeReals × NonnegativeReals) (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals))
               (λ x : NonnegativeReals × NonnegativeReals,
                      pr1 x - pr2 x ,, pr2 x - pr1 x).
Show proof.
  intros x y.
  apply factor_through_squash.
  { refine (isasetdirprod _ _ _ _ _ _) ;
    apply (pr2 (pr1 (pr1 (pr1 NonnegativeReals)))).
  }
  intros c.
  apply dirprodeq.
  + apply iscomprelfun_NRminus.
    apply (plusNonnegativeReals_eqcompat_l (pr1 c)).
    exact (pr2 c).
  + apply (iscomprelfun_NRminus (pr2 x ,, pr1 x) (pr2 y ,, pr1 y)).
    simpl.
    rewrite (iscomm_plusNonnegativeReals (pr2 x)), (iscomm_plusNonnegativeReals (pr2 y)).
    apply (plusNonnegativeReals_eqcompat_l (pr1 c)), pathsinv0.
    exact (pr2 c).

Definition hr_to_NR (x : hr_commring) : NonnegativeReals × NonnegativeReals.
Show proof.
  revert x.
  simple refine (setquotuniv _ (_,,_) _ _).
  - apply isasetdirprod ;
    apply (pr2 (pr1 (pr1 (pr1 NonnegativeReals)))).
  - intros x.
    apply (pr1 x - pr2 x ,, pr2 x - pr1 x).
  - apply iscomprelfun_hr_to_NR.

Definition hr_to_NRpos (x : hr_commring) : NonnegativeReals := pr1 (hr_to_NR x).
Definition hr_to_NRneg (x : hr_commring) : NonnegativeReals := pr2 (hr_to_NR x).

Lemma hr_to_NR_correct :
  ∏ (x : hr_commring), pr1 x (hr_to_NR x).
Show proof.
  intros X.
  generalize (pr1 (pr2 X)).
  apply hinhuniv.
  intros x.
  pattern X at 2.
  rewrite <- (setquotl0 _ X x).
  unfold hr_to_NR.
  rewrite setquotunivcomm.
  generalize (pr2 x).
  apply (pr1 (pr2 (pr2 X))).
  apply hinhpr.
  exists 0 ; simpl.
  change ((pr1 (pr1 x) + (pr2 (pr1 x) - pr1 (pr1 x)) + 0) =
   ((pr1 (pr1 x) - pr2 (pr1 x)) + pr2 (pr1 x) + 0))%NR.
  rewrite !isrunit_zero_plusNonnegativeReals.
  rewrite iscomm_plusNonnegativeReals, <- !maxNonnegativeReals_minus_plus.
  now apply iscomm_maxNonnegativeReals.

Lemma hr_to_NRpos_NR_to_hr :
  ∏ (x : NonnegativeReals × NonnegativeReals),
    hr_to_NRpos (NR_to_hr x) = pr1 x - pr2 x.
Show proof.
  intros x.
  unfold hr_to_NRpos, hr_to_NR, NR_to_hr.
  now rewrite setquotunivcomm.
Lemma hr_to_NRneg_NR_to_hr :
  ∏ (x : NonnegativeReals × NonnegativeReals),
    hr_to_NRneg (NR_to_hr x) = pr2 x - pr1 x.
Show proof.
  intros x.
  unfold hr_to_NRneg, hr_to_NR, NR_to_hr.
  now rewrite setquotunivcomm.

Lemma hr_to_NR_bij :
  ∏ x : hr_commring, NR_to_hr (hr_to_NR x) = x.
Show proof.
  intros x.
  unfold NR_to_hr.
  pattern x at 2.
  apply (setquotl0 _ x ((hr_to_NR x),,(hr_to_NR_correct x))).

Lemma hr_to_NRposneg_zero :
  ∏ x : hr_commring, 0 < hr_to_NRpos x -> hr_to_NRneg x = 0.
Show proof.
  intros x.
  rewrite <- (hr_to_NR_bij x).
  generalize (hr_to_NR x) ; clear x ; intros x.
  rewrite hr_to_NRpos_NR_to_hr, hr_to_NRneg_NR_to_hr.
  intros Hx.
  apply minusNonnegativeReals_eq_zero.
  apply lt_leNonnegativeReals.
  apply_pr2 ispositive_minusNonnegativeReals.
  exact Hx.
Lemma hr_to_NRnegpos_zero :
  ∏ x : hr_commring, 0 < hr_to_NRneg x -> hr_to_NRpos x = 0.
Show proof.
  intros x.
  rewrite <- (hr_to_NR_bij x).
  generalize (hr_to_NR x) ; clear x ; intros x.
  rewrite hr_to_NRpos_NR_to_hr, hr_to_NRneg_NR_to_hr.
  intros Hx.
  apply minusNonnegativeReals_eq_zero.
  apply lt_leNonnegativeReals.
  apply_pr2 ispositive_minusNonnegativeReals.
  exact Hx.

Lemma hr_to_NRpos_NR_to_hr_std :
  ∏ (x : NonnegativeReals × NonnegativeReals),
    (0 < pr1 x -> pr2 x = 0) ->
    hr_to_NRpos (NR_to_hr x) = pr1 x.
Show proof.
  intros x Hx.
  rewrite hr_to_NRpos_NR_to_hr.
  apply (plusNonnegativeReals_eqcompat_l (pr2 x)).
  rewrite <- maxNonnegativeReals_minus_plus.
  now apply max_plusNonnegativeReals.
Lemma hr_to_NRneg_NR_to_hr_std :
  ∏ (x : NonnegativeReals × NonnegativeReals),
    (0 < pr1 x -> pr2 x = 0) ->
    hr_to_NRneg (NR_to_hr x) = pr2 x.
Show proof.
  intros x Hx.
  rewrite hr_to_NRneg_NR_to_hr.
  apply (plusNonnegativeReals_eqcompat_l (pr1 x)).
  rewrite <- maxNonnegativeReals_minus_plus.
  rewrite iscomm_plusNonnegativeReals, iscomm_maxNonnegativeReals.
  now apply max_plusNonnegativeReals.

Caracterisation of equality

Lemma NR_to_hr_eq :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    pr1 x + pr2 y = pr1 y + pr2 x <-> NR_to_hr x = NR_to_hr y.
Show proof.
  intros x y.
  split ; intros H.
  - apply iscompsetquotpr.
    apply hinhpr.
    exists 0.
    apply_pr2 plusNonnegativeReals_eqcompat_l.
    exact H.
  - generalize (invmap (weqpathsinsetquot _ _ _) H) ; clear H.
    apply factor_through_squash.
    { apply (pr2 (pr1 (pr1 (pr1 NonnegativeReals)))). }
    intros (c,p); generalize p; clear p.
    apply plusNonnegativeReals_eqcompat_l.

Constants and Operations

0

Lemma hr_to_NR_zero :
  hr_to_NR 0%ring = (0,,0).
Show proof.
  unfold ringunel1, unel_is ; simpl.
  unfold hr_to_NR.
  refine (setquotunivcomm _ (_ ,, _) _ _ _ @ _) ; simpl.
  rewrite !minusNonnegativeReals_eq_zero.
  { reflexivity. }
  apply isrefl_leNonnegativeReals.

1

Lemma hr_to_NR_one :
  hr_to_NR 1%ring = (1,,0).
Show proof.
  unfold ringunel2, unel_is ; simpl.
  unfold rigtoringunel2, hr_to_NR.
  rewrite setquotunivcomm ; simpl.
  erewrite <- minusNonnegativeReals_correct_r.
  - rewrite minusNonnegativeReals_eq_zero.
    + reflexivity.
    + apply isnonnegative_NonnegativeReals.
  - apply pathsinv0, isrunit_zero_plusNonnegativeReals.

plus

Lemma NR_to_hr_plus :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    (NR_to_hr x + NR_to_hr y)%ring = NR_to_hr (pr1 x + pr1 y ,, pr2 x + pr2 y).
Show proof.
  intros x y.
  unfold BinaryOperations.op1 ; simpl.
  unfold rigtoringop1 ; simpl.
  unfold NR_to_hr.
  apply (setquotfun2comm (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals)) (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals))).

opp

Lemma NR_to_hr_opp :
  ∏ x : NonnegativeReals × NonnegativeReals,
    (- NR_to_hr x)%ring = NR_to_hr (pr2 x ,, pr1 x).
Show proof.
  intros x.
  unfold ringinv1, grinv_is ; simpl.
  unfold abgrdiffinv.
  unfold NR_to_hr.
  apply (setquotfuncomm (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals)) (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals))).

Lemma hr_to_NR_opp :
  ∏ x : hr_commring,
    hr_to_NR (- x)%ring = (hr_to_NRneg x ,, hr_to_NRpos x).
Show proof.
  intros x.
  rewrite <- (hr_to_NR_bij x), NR_to_hr_opp.
  unfold hr_to_NRneg, hr_to_NRpos.
  generalize (hr_to_NR x) ; clear x ; intros x.
  unfold hr_to_NR, NR_to_hr.
  rewrite !setquotunivcomm.
  reflexivity.
Lemma hr_to_NRpos_opp :
  ∏ x : hr_commring,
    hr_to_NRpos (- x)%ring = hr_to_NRneg x.
Show proof.
  intros x.
  unfold hr_to_NRpos.
  now rewrite hr_to_NR_opp.
Lemma hr_to_NRneg_opp :
  ∏ x : hr_commring,
    hr_to_NRneg (- x)%ring = hr_to_NRpos x.
Show proof.
  intros x.
  unfold hr_to_NRneg.
  now rewrite hr_to_NR_opp.

minus

Lemma NR_to_hr_minus :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    (NR_to_hr x - NR_to_hr y)%ring = NR_to_hr (pr1 x + pr2 y ,, pr2 x + pr1 y).
Show proof.
  intros x y.
  rewrite NR_to_hr_opp, NR_to_hr_plus.
  reflexivity.

Lemma hr_opp_minus :
  ∏ x y : hr_commring,
    (x - y = - ((- x) - (- y)))%ring.
Show proof.
  intros x y.
  rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij y).
  rewrite !NR_to_hr_opp, !NR_to_hr_plus, NR_to_hr_opp ; simpl.
  reflexivity.

Lemma hr_to_NRpos_minus :
  ∏ x y : hr_commring,
    hr_to_NRpos x - hr_to_NRpos y <= hr_to_NRpos (x - y)%ring.
Show proof.
  intros X Y.
  set (x := hr_to_NRpos X) ;
  set (y := hr_to_NRpos Y).
  rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y).
  rewrite NR_to_hr_minus.
  change (pr1 (hr_to_NR X)) with x.
  change (pr1 (hr_to_NR Y)) with y.
  change (pr2 (hr_to_NR X)) with (hr_to_NRneg X).
  change (pr2 (hr_to_NR Y)) with (hr_to_NRneg Y).
  rewrite hr_to_NRpos_NR_to_hr.
  simpl pr1 ; simpl pr2.
  apply_pr2 (plusNonnegativeReals_lecompat_l (hr_to_NRneg X + y)).
  rewrite <- maxNonnegativeReals_minus_plus.
  rewrite (iscomm_plusNonnegativeReals _ y), <- isassoc_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus.
  rewrite isrdistr_max_plusNonnegativeReals.
  apply maxNonnegativeReals_le.
  - rewrite <- max_plusNonnegativeReals.
    + apply maxNonnegativeReals_le.
      * eapply istrans_leNonnegativeReals, maxNonnegativeReals_le_l.
        apply plusNonnegativeReals_le_l.
      * eapply istrans_leNonnegativeReals, maxNonnegativeReals_le_r.
        apply plusNonnegativeReals_le_r.
    + apply hr_to_NRposneg_zero.
  - apply maxNonnegativeReals_le_r.
Lemma hr_to_NRneg_minus :
  ∏ x y : hr_commring,
    hr_to_NRneg x - hr_to_NRneg y <= hr_to_NRneg (x - y)%ring.
Show proof.
  intros x y.
  rewrite hr_opp_minus.
  pattern x at 1 ;
    rewrite <- (grinvinv hr_commring x) ;
    pattern y at 1 ;
    rewrite <- (grinvinv hr_commring y).
  change (hr_to_NRneg (- (- x))%ring - hr_to_NRneg (- (- y))%ring <=
   hr_to_NRneg (- (- x - - y))%ring).
  rewrite !hr_to_NRneg_opp.
  apply hr_to_NRpos_minus.

mult

Lemma NR_to_hr_mult :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    (NR_to_hr x * NR_to_hr y)%ring = NR_to_hr (pr1 x * pr1 y + pr2 x * pr2 y ,, pr1 x * pr2 y + pr2 x * pr1 y).
Show proof.
  intros x y.
  unfold BinaryOperations.op2 ; simpl.
  unfold rigtoringop2 ; simpl.
  unfold NR_to_hr.
  apply (setquotfun2comm (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals)) (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals))).

Order

hr_lt_rel

Local Lemma isbinophrel_ltNonnegativeReals :
  isbinophrel (X := rigaddabmonoid NonnegativeReals) ltNonnegativeReals.
Show proof.
  split.
  - intros x y z Hlt.
    apply plusNonnegativeReals_ltcompat_r, Hlt.
  - intros x y z Hlt.
    apply plusNonnegativeReals_ltcompat_l, Hlt.
Definition hr_lt_rel : hrel hr_commring
  := rigtoringrel NonnegativeReals isbinophrel_ltNonnegativeReals.

Lemma NR_to_hr_lt :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    pr1 x + pr2 y < pr1 y + pr2 x
    <-> hr_lt_rel (NR_to_hr x) (NR_to_hr y).
Show proof.
  intros x y.
  split.
  - intros H.
    apply hinhpr ; exists 0 ; simpl.
    apply plusNonnegativeReals_ltcompat_l, H.
  - apply hinhuniv ; intros H.
    apply_pr2 (plusNonnegativeReals_ltcompat_l (pr1 H)).
    exact (pr2 H).

hr_le_rel

Local Lemma isbinophrel_leNonnegativeReals :
  isbinophrel (X := rigaddabmonoid NonnegativeReals) leNonnegativeReals.
Show proof.
  split.
  - intros x y z Hlt.
    apply plusNonnegativeReals_lecompat_r, Hlt.
  - intros x y z Hlt.
    apply plusNonnegativeReals_lecompat_l, Hlt.
Definition hr_le_rel : hrel hr_commring
  := rigtoringrel NonnegativeReals isbinophrel_leNonnegativeReals.

Lemma NR_to_hr_le :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    pr1 x + pr2 y <= pr1 y + pr2 x
    <-> hr_le_rel (NR_to_hr x) (NR_to_hr y).
Show proof.
  intros x y.
  split.
  - intros H.
    apply hinhpr ; exists 0 ; simpl.
    apply plusNonnegativeReals_lecompat_l, H.
  - apply hinhuniv ; intros H.
    apply_pr2 (plusNonnegativeReals_lecompat_l (pr1 H)).
    exact (pr2 H).

Theorems about order

Lemma hr_notlt_le :
  ∏ X Y, ¬ hr_lt_rel X Y <-> hr_le_rel Y X.
Show proof.
  intros x y.
  rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij y).
  split ; intro H.
  - apply NR_to_hr_le.
    apply notlt_leNonnegativeReals.
    intro H0 ; apply H.
    apply NR_to_hr_lt.
    exact H0.
  - intro H0.
    refine (pr2 (notlt_leNonnegativeReals _ _) _ _).
    + refine (pr2 (NR_to_hr_le _ _) _).
      apply H.
    + apply_pr2 NR_to_hr_lt.
      exact H0.

Lemma hr_lt_le :
  ∏ X Y, hr_lt_rel X Y -> hr_le_rel X Y.
Show proof.
  intros x y.
  rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij y).
  intro H.
  apply NR_to_hr_le.
  apply lt_leNonnegativeReals.
  apply_pr2 NR_to_hr_lt.
  exact H.

Lemma isantisymm_hr_le :
  isantisymm hr_le_rel.
Show proof.
  apply isantisymmabgrdiffrel.
  intros X Y Hxy Hyx.
  apply isantisymm_leNonnegativeReals.
  now split.

Lemma isStrongOrder_hr_lt : isStrongOrder hr_lt_rel.
Show proof.
  apply isStrongOrder_abgrdiff.
  repeat split.
  - exact istrans_ltNonnegativeReals.
  - exact iscotrans_ltNonnegativeReals.
  - exact isirrefl_ltNonnegativeReals.

Lemma iscotrans_hr_lt :
  iscotrans hr_lt_rel.
Show proof.
  apply iscotrans_isStrongOrder.
  apply isStrongOrder_hr_lt.

Lemma hr_to_NR_nonnegative :
  ∏ x : hr_commring,
    (hr_to_NRneg x = 0) <-> hr_le_rel 0%ring x.
Show proof.
  intros x.
  pattern x at 2.
  rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero.
  unfold hr_to_NRneg.
  split.
  - generalize (hr_to_NR x). intros hx.
    change hx with (pr1 hx,,pr2 hx).
    generalize (pr1 hx), (pr2 hx).
    clear hx.
    intros x1 x2 ; simpl pr1 ; simpl pr2 ; clear x ; intros ->.
    apply NR_to_hr_le ; simpl.
    rewrite !isrunit_zero_plusNonnegativeReals.
    now apply isnonnegative_NonnegativeReals.
  - pattern x at 2.
    rewrite <- (hr_to_NR_bij x).
    generalize (hr_to_NR x) ; clear x ; intros x Hx.
    unfold hr_to_NR, NR_to_hr.
    rewrite setquotunivcomm ; simpl.
    apply_pr2_in NR_to_hr_le Hx.
    rewrite isrunit_zero_plusNonnegativeReals, islunit_zero_plusNonnegativeReals in Hx.
    now apply minusNonnegativeReals_eq_zero.

Lemma hr_to_NR_positive :
  ∏ x : hr_commring,
    (hr_to_NRpos x ≠ 0 × hr_to_NRneg x = 0) <-> hr_lt_rel 0%ring x.
Show proof.
  intros x.
  repeat split.
  - pattern x at 3.
    rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero.
    unfold hr_to_NRpos, hr_to_NRneg.
    change (hr_to_NR x) with (pr1 (hr_to_NR x),,pr2 _).
    generalize (pr1 (hr_to_NR x)), (pr2 (hr_to_NR x)) ;
      intros x1 x2 ; simpl pr1 ; simpl pr2 ; clear x ; intros H1 ; rewrite (pr2 H1).
    apply NR_to_hr_lt ; simpl.
    rewrite !isrunit_zero_plusNonnegativeReals.
    now apply ispositive_apNonnegativeReals, (pr1 H1).
  - rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero in X.
    apply_pr2_in NR_to_hr_lt X.
    rewrite isrunit_zero_plusNonnegativeReals, islunit_zero_plusNonnegativeReals in X.
    apply_pr2 ispositive_apNonnegativeReals.
    eapply istrans_le_lt_ltNonnegativeReals, X.
    now apply isnonnegative_NonnegativeReals.
  - apply_pr2 hr_to_NR_nonnegative.
    now apply hr_lt_le.

Lemma hr_to_NR_nonpositive :
  ∏ x : hr_commring,
    (hr_to_NRpos x = 0) <-> hr_le_rel x 0%ring.
Show proof.
  intros x.
  pattern x at 2.
  rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero.
  unfold hr_to_NRpos.
  split.
  - change (hr_to_NR x) with (pr1 (hr_to_NR x),,pr2 _).
    simpl pr1 ; simpl pr2 ; intros ->.
    apply NR_to_hr_le ; simpl.
    rewrite !islunit_zero_plusNonnegativeReals.
    now apply isnonnegative_NonnegativeReals.
  - pattern x at 2.
    rewrite <- (hr_to_NR_bij x).
    generalize (hr_to_NR x) ; clear x ; intros x Hx.
    unfold hr_to_NR, NR_to_hr.
    rewrite setquotunivcomm ; simpl.
    apply_pr2_in NR_to_hr_le Hx.
    rewrite isrunit_zero_plusNonnegativeReals, islunit_zero_plusNonnegativeReals in Hx.
    now apply minusNonnegativeReals_eq_zero.

Lemma hr_to_NR_negative :
  ∏ x : hr_commring,
    (hr_to_NRpos x = 0 × hr_to_NRneg x ≠ 0) <-> hr_lt_rel x 0%ring.
Show proof.
  intros x.
  repeat split.
  - pattern x at 3.
    rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero.
    unfold hr_to_NRpos, hr_to_NRneg.
    change (hr_to_NR x) with (pr1 (hr_to_NR x),,pr2 _).
    simpl pr1 ; simpl pr2 ; intros H2 ; rewrite (pr1 H2).
    apply NR_to_hr_lt ; simpl.
    rewrite !islunit_zero_plusNonnegativeReals.
    now apply ispositive_apNonnegativeReals, (pr2 H2).
  - apply_pr2 hr_to_NR_nonpositive.
    now apply hr_lt_le.
  - rewrite <- (hr_to_NR_bij x), <- (hr_to_NR_bij 0%ring), hr_to_NR_zero in X.
    apply_pr2_in NR_to_hr_lt X.
    rewrite isrunit_zero_plusNonnegativeReals, islunit_zero_plusNonnegativeReals in X.
    apply_pr2 ispositive_apNonnegativeReals.
    eapply istrans_le_lt_ltNonnegativeReals, X.
    now apply isnonnegative_NonnegativeReals.

Lemma hr_plus_ltcompat_l :
  ∏ x y z : hr_commring, hr_lt_rel y z <-> hr_lt_rel (y+x)%ring (z+x)%ring.
Show proof.
  intros X Y Z.
  rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y), <- (hr_to_NR_bij Z).
  rewrite !NR_to_hr_plus.
  split ; intro Hlt.
  - apply NR_to_hr_lt ; simpl.
    rewrite !(iscomm_plusNonnegativeReals _ (pr1 (hr_to_NR X))), !isassoc_plusNonnegativeReals.
    apply plusNonnegativeReals_ltcompat_r.
    rewrite <- ! isassoc_plusNonnegativeReals.
    apply plusNonnegativeReals_ltcompat_l.
    now apply_pr2 NR_to_hr_lt.
  - apply NR_to_hr_lt ; simpl.
    apply_pr2 (plusNonnegativeReals_ltcompat_l (pr2 (hr_to_NR X))).
    apply_pr2 (plusNonnegativeReals_ltcompat_r (pr1 (hr_to_NR X))).
    rewrite <- ! isassoc_plusNonnegativeReals.
    rewrite !(iscomm_plusNonnegativeReals (pr1 (hr_to_NR X))), !(isassoc_plusNonnegativeReals (_ + pr1 (hr_to_NR X))).
    now apply_pr2_in NR_to_hr_lt Hlt.
Lemma hr_plus_ltcompat_r :
  ∏ x y z : hr_commring, hr_lt_rel y z <-> hr_lt_rel (x + y)%ring (x + z)%ring.
Show proof.
  intros x y z.
  rewrite !(ringcomm1 _ x).
  apply hr_plus_ltcompat_l.

Lemma hr_plus_lecompat_l :
  ∏ x y z : hr_commring, hr_le_rel y z <-> hr_le_rel (y + x)%ring (z + x)%ring.
Show proof.
  intros x y z ; split ; intro Hle.
  - apply hr_notlt_le.
    apply_pr2_in hr_notlt_le Hle.
    intro Hlt ; apply Hle.
    apply_pr2 (hr_plus_ltcompat_l x).
    exact Hlt.
  - apply hr_notlt_le.
    apply_pr2_in hr_notlt_le Hle.
    intro Hlt ; apply Hle.
    apply hr_plus_ltcompat_l.
    exact Hlt.
Lemma hr_plus_lecompat_r :
  ∏ x y z : hr_commring, hr_le_rel y z <-> hr_le_rel (x + y)%ring (x + z)%ring.
Show proof.
  intros x y z.
  rewrite !(ringcomm1 _ x).
  apply hr_plus_lecompat_l.

Lemma hr_mult_ltcompat_l :
  ∏ x y z : hr_commring, hr_lt_rel 0%ring x -> hr_lt_rel y z -> hr_lt_rel (y * x)%ring (z * x)%ring.
Show proof.
  intros X Y Z Hx0 Hlt.
  apply_pr2_in hr_to_NR_positive Hx0.
  rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y), <- (hr_to_NR_bij Z).
  rewrite !NR_to_hr_mult ; simpl pr1 ; simpl pr2.
  change (pr2 (hr_to_NR X)) with (hr_to_NRneg X) ;
  rewrite (pr2 Hx0).
  rewrite !israbsorb_zero_multNonnegativeReals, !isrunit_zero_plusNonnegativeReals, !islunit_zero_plusNonnegativeReals.
  apply NR_to_hr_lt ; simpl.
  rewrite <- !isrdistr_plus_multNonnegativeReals.
  apply multNonnegativeReals_ltcompat_l.
  - apply ispositive_apNonnegativeReals.
    exact (pr1 Hx0).
  - apply_pr2 NR_to_hr_lt.
    now rewrite !hr_to_NR_bij.
Lemma hr_mult_ltcompat_l' :
  ∏ x y z : hr_commring, hr_le_rel 0%ring x -> hr_lt_rel (y * x)%ring (z * x)%ring -> hr_lt_rel y z.
Show proof.
  intros X Y Z Hx0.
  apply_pr2_in hr_to_NR_nonnegative Hx0.
  rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y), <- (hr_to_NR_bij Z).
  rewrite !NR_to_hr_mult ; simpl pr1 ; simpl pr2.
  change (pr2 (hr_to_NR X)) with (hr_to_NRneg X).
  rewrite Hx0.
  rewrite !israbsorb_zero_multNonnegativeReals, !isrunit_zero_plusNonnegativeReals, !islunit_zero_plusNonnegativeReals.
  intros Hlt.
  apply NR_to_hr_lt.
  apply multNonnegativeReals_ltcompat_l' with (pr1 (hr_to_NR X)).
  rewrite !isrdistr_plus_multNonnegativeReals.
  now apply_pr2_in NR_to_hr_lt Hlt.
Lemma hr_mult_ltcompat_r' :
  ∏ x y z : hr_commring, hr_le_rel 0%ring x -> hr_lt_rel (x * y)%ring (x * z)%ring -> hr_lt_rel y z.
Show proof.
  intros x y z.
  rewrite !(ringcomm2 _ x).
  apply hr_mult_ltcompat_l'.

Lemma hr_mult_lecompat_l :
  ∏ x y z : hr_commring, hr_le_rel 0%ring x -> hr_le_rel y z -> hr_le_rel (y * x)%ring (z * x)%ring.
Show proof.
  intros x y z Hx0 Hle.
  apply hr_notlt_le.
  apply_pr2_in hr_notlt_le Hle.
  intro Hlt ; apply Hle.
  apply (hr_mult_ltcompat_l' x).
  - exact Hx0.
  - exact Hlt.
Lemma hr_mult_lecompat_l' :
  ∏ x y z : hr_commring, hr_lt_rel 0%ring x -> hr_le_rel (y * x)%ring (z * x)%ring -> hr_le_rel y z.
Show proof.
  intros x y z Hx0 Hle.
  apply hr_notlt_le.
  apply_pr2_in hr_notlt_le Hle.
  intro Hlt ; apply Hle.
  apply (hr_mult_ltcompat_l x).
  - exact Hx0.
  - exact Hlt.
Lemma hr_mult_lecompat_r :
  ∏ x y z : hr_commring, hr_le_rel 0%ring x -> hr_le_rel y z -> hr_le_rel (x * y)%ring (x * z)%ring.
Show proof.
  intros x y z.
  rewrite !(ringcomm2 _ x).
  apply hr_mult_lecompat_l.
Lemma hr_mult_lecompat_r' :
  ∏ x y z : hr_commring, hr_lt_rel 0%ring x -> hr_le_rel (x * y)%ring (x * z)%ring -> hr_le_rel y z.
Show proof.
  intros x y z.
  rewrite !(ringcomm2 _ x).
  apply hr_mult_lecompat_l'.

Appartness


Local Lemma isbinophrel_apNonnegativeReals :
  isbinophrel (X := rigaddabmonoid NonnegativeReals) apNonnegativeReals.
Show proof.
  split.
  - intros x y z Hlt.
    apply plusNonnegativeReals_apcompat_r, Hlt.
  - intros x y z Hlt.
    apply plusNonnegativeReals_apcompat_l, Hlt.
Definition hr_ap_rel : hrel hr_commring
  := rigtoringrel NonnegativeReals isbinophrel_apNonnegativeReals.

Lemma NR_to_hr_ap :
  ∏ x y : NonnegativeReals × NonnegativeReals,
    pr1 x + pr2 y ≠ pr1 y + pr2 x
    <-> hr_ap_rel (NR_to_hr x) (NR_to_hr y).
Show proof.
  intros x y.
  split.
  - intros H.
    apply hinhpr ; exists 0 ; simpl.
    apply plusNonnegativeReals_apcompat_l, H.
  - apply hinhuniv ; intros H.
    apply_pr2 (plusNonnegativeReals_apcompat_l (pr1 H)).
    exact (pr2 H).

Theorems about apartness

Lemma hr_ap_lt :
  ∏ X Y : hr_commring, hr_ap_rel X Y <-> (hr_lt_rel X Y) ⨿ (hr_lt_rel Y X).
Show proof.
  intros X Y.
  rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y).
  split ; intro Hap.
  - apply_pr2_in NR_to_hr_ap Hap.
    revert Hap.
    apply sumofmaps ; intros Hlt.
    + now left ; apply NR_to_hr_lt.
    + now right ; apply NR_to_hr_lt.
  - apply NR_to_hr_ap.
    revert Hap ; apply sumofmaps ; intros Hlt.
    + now left ; apply_pr2 NR_to_hr_lt.
    + now right ; apply_pr2 NR_to_hr_lt.

Lemma istightap_hr_ap : istightap hr_ap_rel.
Show proof.
  repeat split.
  - intros X Hap.
    rewrite <- (hr_to_NR_bij X) in Hap.
    apply_pr2_in NR_to_hr_ap Hap.
    revert Hap.
    now apply isirrefl_apNonnegativeReals.
  - intros X Y.
    rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y).
    intros Hap.
    apply NR_to_hr_ap.
    apply issymm_apNonnegativeReals.
    now apply_pr2 NR_to_hr_ap.
  - intros X Y Z Hap.
    apply hr_ap_lt in Hap.
    revert Hap ; apply sumofmaps ; intros Hlt.
    + apply (iscotrans_hr_lt X Y Z) in Hlt.
      revert Hlt ; apply hinhfun ; apply sumofmaps ; intros Hlt.
      * left ; apply_pr2 hr_ap_lt.
        now left.
      * right ; apply_pr2 hr_ap_lt.
        now left.
    + apply (iscotrans_hr_lt _ Y _) in Hlt.
      revert Hlt ; apply hinhfun ; apply sumofmaps ; intros Hlt.
      * right ; apply_pr2 hr_ap_lt.
        now right.
      * left ; apply_pr2 hr_ap_lt.
        now right.
  - intros X Y Hap.
    apply isantisymm_hr_le.
    + apply hr_notlt_le.
      intro Hlt ; apply Hap.
      apply_pr2 hr_ap_lt.
      now right.
    + apply hr_notlt_le.
      intro Hlt ; apply Hap.
      apply_pr2 hr_ap_lt.
      now left.

Structures

Lemma islapbinop_plus : islapbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op1.
Show proof.
  intros X Y Z.
  unfold tightapSet_rel ; simpl pr1.
  intro Hap.
  apply_pr2 hr_ap_lt.
  apply hr_ap_lt in Hap.
  revert Hap ; apply sumofmaps ; intros Hlt.
  - left.
    apply_pr2 (hr_plus_ltcompat_l X).
    exact Hlt.
  - right.
    apply_pr2 (hr_plus_ltcompat_l X).
    exact Hlt.
Lemma israpbinop_plus : israpbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op1.
Show proof.
  intros X Y Z Hap.
  apply islapbinop_plus with X.
  rewrite !(ringcomm1 _ _ X).
  exact Hap.

Lemma islapbinop_mult : islapbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op2.
Show proof.
  intros X Y Z.
  unfold tightapSet_rel ; simpl pr1.
  rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y), <- (hr_to_NR_bij Z), !NR_to_hr_mult.
  intros Hap.
  apply_pr2_in NR_to_hr_ap Hap ; simpl in Hap.
  cut (∏ Y Z, (pr1 (hr_to_NR Z) * pr1 (hr_to_NR X) + pr2 (hr_to_NR Z) * pr2 (hr_to_NR X) + (pr1 (hr_to_NR Y) * pr2 (hr_to_NR X) + pr2 (hr_to_NR Y) * pr1 (hr_to_NR X)))
       = (pr1 (hr_to_NR Z) + pr2 (hr_to_NR Y)) * pr1 (hr_to_NR X) + (pr2 (hr_to_NR Z) + pr1 (hr_to_NR Y)) * pr2 (hr_to_NR X)).
  - intro H ; simpl in H,Hap ; rewrite !H in Hap ; clear H.
    apply ap_plusNonnegativeReals in Hap.
    apply NR_to_hr_ap.
    revert Hap ; apply hinhuniv ; apply sumofmaps ; intros Hap.
    + apply ap_multNonnegativeReals in Hap.
      revert Hap ; apply hinhuniv ; apply sumofmaps ; intros Hap.
      * exact Hap.
      * now eapply fromempty, (isirrefl_apNonnegativeReals _), Hap .
    + apply ap_multNonnegativeReals in Hap.
      revert Hap ; apply hinhuniv ; apply sumofmaps ; intros Hap.
      * rewrite (iscomm_plusNonnegativeReals (pr1 (hr_to_NR Z))), iscomm_plusNonnegativeReals.
        now apply issymm_apNonnegativeReals, Hap.
      * now eapply fromempty, (isirrefl_apNonnegativeReals _), Hap.
  - clear ; intros Y Z.
    rewrite !isrdistr_plus_multNonnegativeReals.
    rewrite !isassoc_plusNonnegativeReals.
    apply_pr2 plusNonnegativeReals_eqcompat_r.
    do 2 rewrite iscomm_plusNonnegativeReals, !isassoc_plusNonnegativeReals.
    reflexivity.
Lemma israpbinop_mult : israpbinop (X := _,,_,,istightap_hr_ap) BinaryOperations.op2.
Show proof.
  intros X Y Z Hap.
  apply islapbinop_mult with X.
  rewrite !(ringcomm2 _ _ X).
  exact Hap.

Lemma hr_ap_0_1 :
  isnonzeroCR hr_commring (hr_ap_rel,, istightap_hr_ap).
Show proof.
  change (hr_ap_rel 1%ring 0%ring).
  rewrite <- (hr_to_NR_bij 1%ring), <- (hr_to_NR_bij 0%ring), hr_to_NR_one, hr_to_NR_zero.
  apply NR_to_hr_ap.
  rewrite !isrunit_zero_plusNonnegativeReals.
  apply isnonzeroNonnegativeReals.

Lemma hr_islinv_neg :
  ∏ (x : hr_commring) (Hap : hr_lt_rel x 0%ring),
   (NR_to_hr (0%NR,, invNonnegativeReals (hr_to_NRneg x) (pr2 (pr2 (hr_to_NR_negative _) Hap))) * x)%ring = 1%ring.
Show proof.
  intros x Hap.
  pattern x at 3;
    rewrite <- (hr_to_NR_bij x).
  rewrite NR_to_hr_mult ; simpl.
  rewrite !islabsorb_zero_multNonnegativeReals , !islunit_zero_plusNonnegativeReals.
  rewrite islinv_invNonnegativeReals.
  rewrite <- (hr_to_NR_bij 1%ring), hr_to_NR_one.
  apply maponpaths.
  apply maponpaths.
  erewrite <- israbsorb_zero_multNonnegativeReals.
  apply maponpaths.
  apply (pr1 (pr2 (hr_to_NR_negative x) Hap)).
Lemma hr_isrinv_neg :
  ∏ (x : hr_commring) (Hap : hr_lt_rel x 0%ring),
   (x * NR_to_hr (0%NR,, invNonnegativeReals (hr_to_NRneg x) (pr2 (pr2 (hr_to_NR_negative _) Hap))))%ring = 1%ring.
Show proof.
  intros x Hap.
  rewrite ringcomm2.
  now apply (hr_islinv_neg x Hap).

Lemma hr_islinv_pos :
  ∏ (x : hr_commring) (Hap : hr_lt_rel 0%ring x),
   (NR_to_hr (invNonnegativeReals (hr_to_NRpos x) (pr1 (pr2 (hr_to_NR_positive _) Hap)) ,, 0%NR) * x)%ring = 1%ring.
Show proof.
  intros x Hap.
  pattern x at 3;
    rewrite <- (hr_to_NR_bij x).
  rewrite NR_to_hr_mult ; simpl.
  rewrite !islabsorb_zero_multNonnegativeReals , !isrunit_zero_plusNonnegativeReals.
  rewrite islinv_invNonnegativeReals.
  rewrite <- (hr_to_NR_bij 1%ring), hr_to_NR_one.
  apply maponpaths.
  apply maponpaths.
  erewrite <- israbsorb_zero_multNonnegativeReals.
  apply maponpaths.
  apply (pr2 (pr2 (hr_to_NR_positive x) Hap)).
Lemma hr_isrinv_pos :
  ∏ (x : hr_commring) (Hap : hr_lt_rel 0%ring x),
   (x * NR_to_hr (invNonnegativeReals (hr_to_NRpos x) (pr1 (pr2 (hr_to_NR_positive _) Hap)) ,, 0%NR))%ring = 1%ring.
Show proof.
  intros x Hap.
  rewrite ringcomm2.
  now apply (hr_islinv_pos x Hap).

Lemma hr_ex_inv :
  ∏ x : hr_commring,
    hr_ap_rel x 0%ring -> multinvpair hr_commring x.
Show proof.
  intros x Hap.
  generalize (pr1 (hr_ap_lt _ _) Hap) ;
    apply sumofmaps ; intros Hlt ; simpl.
  - eexists ; split.
    + refine (hr_islinv_neg _ _).
      exact Hlt.
    + exact (hr_isrinv_neg _ _).
  - eexists ; split.
    + refine (hr_islinv_pos _ _).
      exact Hlt.
    + exact (hr_isrinv_pos _ _).

Definition hr_ConstructiveField : ConstructiveField.
Show proof.
  exists hr_commring.
  exists (_,,istightap_hr_ap).
  repeat split.
  - exact islapbinop_plus.
  - exact israpbinop_plus.
  - exact islapbinop_mult.
  - exact israpbinop_mult.
  - exact hr_ap_0_1.
  - exact hr_ex_inv.

hr_abs


Definition hr_abs (x : hr_ConstructiveField) : NonnegativeReals :=
  maxNonnegativeReals (hr_to_NRpos x) (hr_to_NRneg x).

Lemma NR_to_hr_abs :
  ∏ x : NonnegativeReals × NonnegativeReals,
    hr_abs (NR_to_hr x) <= maxNonnegativeReals (pr1 x) (pr2 x).
Show proof.
  intros x.
  unfold hr_abs.
  rewrite hr_to_NRpos_NR_to_hr, hr_to_NRneg_NR_to_hr.
  apply maxNonnegativeReals_le.
  - eapply istrans_leNonnegativeReals, maxNonnegativeReals_le_l.
    now apply minusNonnegativeReals_le.
  - eapply istrans_leNonnegativeReals, maxNonnegativeReals_le_r.
    now apply minusNonnegativeReals_le.

Lemma hr_abs_opp :
  ∏ x : hr_ConstructiveField, hr_abs (- x)%ring = hr_abs x.
Show proof.
  intros x.
  unfold hr_abs.
  rewrite hr_to_NRpos_opp, hr_to_NRneg_opp.
  apply iscomm_maxNonnegativeReals.

Lemma istriangle_hr_abs :
  ∏ x y : hr_ConstructiveField,
    hr_abs (x + y)%ring <= hr_abs x + hr_abs y.
Show proof.
  intros x y.
  pattern x at 1 ; rewrite <- (hr_to_NR_bij x) ;
  pattern y at 1 ; rewrite <- (hr_to_NR_bij y).
  rewrite NR_to_hr_plus.
  eapply istrans_leNonnegativeReals.
  { apply NR_to_hr_abs. }
  apply maxNonnegativeReals_le ; apply plusNonnegativeReals_lecompat.
  - apply maxNonnegativeReals_le_l.
  - apply maxNonnegativeReals_le_l.
  - apply maxNonnegativeReals_le_r.
  - apply maxNonnegativeReals_le_r.

Lemma istriangle_hr_abs' :
  ∏ x y : hr_ConstructiveField,
    hr_abs x - hr_abs y <= hr_abs (x + y)%ring.
Show proof.
  intros x y.
  apply_pr2 (plusNonnegativeReals_lecompat_l (hr_abs y)).
  rewrite <- maxNonnegativeReals_minus_plus.
  apply maxNonnegativeReals_le.
  - assert (Hx : x = ((x + y) + (- y))%ring).
    { now rewrite ringassoc1, ringrinvax1, ringrunax1. }
    pattern x at 1 ; rewrite Hx.
    rewrite <- (hr_abs_opp y).
    apply istriangle_hr_abs.
  - apply plusNonnegativeReals_le_r.

Lemma hr_abs_minus :
  ∏ x y : hr_ConstructiveField,
    hr_abs x - hr_abs y <= hr_abs (x - y)%ring.
Show proof.
  intros x y.
  rewrite <- (hr_abs_opp y).
  apply istriangle_hr_abs'.

Lemma multNonnegativeReals_lecompat :
  ∏ x y z t : NonnegativeReals, x <= y -> z <= t -> x * z <= y * t.
Show proof.
  intros x y z t H H0.
  eapply istrans_leNonnegativeReals, multNonnegativeReals_lecompat_l', H.
  apply multNonnegativeReals_lecompat_r', H0.
Lemma ispositive_multNonnegativeReals :
  ∏ x y : NonnegativeReals, 0 < x ∧ 0 < y <-> 0 < x * y.
Show proof.
  intros x y.
  split.
  - intros H.
    rewrite <- (islabsorb_zero_multNonnegativeReals y).
    apply multNonnegativeReals_ltcompat_l.
    + apply (pr2 H).
    + apply (pr1 H).
  - intros H ; split.
    + eapply multNonnegativeReals_ltcompat_l'.
      rewrite islabsorb_zero_multNonnegativeReals.
      exact H.
    + eapply multNonnegativeReals_ltcompat_r'.
      rewrite israbsorb_zero_multNonnegativeReals.
      exact H.
Lemma maxNonnegativeReals_lt' :
  ∏ x y z : NonnegativeReals,
    z < maxNonnegativeReals x y -> z < x ∨ z < y.
Show proof.
  intros x y z.
  intros H.
  generalize (iscotrans_ltNonnegativeReals _ x _ H).
  apply hinhfun.
  apply sumofmaps ;
  intros Hx.
  - now left.
  - right.
    rewrite <- (maxNonnegativeReals_carac_r x y).
    + apply H.
    + apply notlt_leNonnegativeReals ; intros Hy.
      apply (isirrefl_ltNonnegativeReals (maxNonnegativeReals x y)).
      apply maxNonnegativeReals_lt.
      * exact Hx.
      * now apply istrans_ltNonnegativeReals with x.

Lemma hr_abs_mult :
  ∏ x y : hr_ConstructiveField, hr_abs (x * y)%ring = hr_abs x * hr_abs y.
Show proof.
  intros x y.
  pattern x at 1 ; rewrite <- (hr_to_NR_bij x) ;
  pattern y at 1 ; rewrite <- (hr_to_NR_bij y).
  rewrite NR_to_hr_mult.
  change (pr1 (hr_to_NR x)) with (hr_to_NRpos x) ;
    change (pr1 (hr_to_NR y)) with (hr_to_NRpos y) ;
    change (pr2 (hr_to_NR x)) with (hr_to_NRneg x) ;
    change (pr2 (hr_to_NR y)) with (hr_to_NRneg y).
  rewrite <- !max_plusNonnegativeReals.
  - unfold hr_abs.
    rewrite hr_to_NRpos_NR_to_hr_std, hr_to_NRneg_NR_to_hr_std ; simpl.
    + rewrite isldistr_max_multNonnegativeReals, !isrdistr_max_multNonnegativeReals.
      rewrite !isassoc_maxNonnegativeReals.
      apply maponpaths.
      rewrite iscomm_maxNonnegativeReals, !isassoc_maxNonnegativeReals.
      rewrite iscomm_maxNonnegativeReals, !isassoc_maxNonnegativeReals.
      apply maponpaths.
      apply iscomm_maxNonnegativeReals.
    + intros H.
      apply maxNonnegativeReals_lt' in H.
      apply le0_NonnegativeReals.
      revert H ; apply hinhuniv ; apply sumofmaps ; intros H ;
        apply_pr2_in ispositive_multNonnegativeReals H ;
        apply maxNonnegativeReals_le ;
        apply_pr2 le0_NonnegativeReals.
      * now rewrite (hr_to_NRposneg_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals.
      * now rewrite (hr_to_NRposneg_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals.
      * now rewrite (hr_to_NRnegpos_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals.
      * now rewrite (hr_to_NRnegpos_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals.
    + intros H.
      apply maxNonnegativeReals_lt' in H.
      apply le0_NonnegativeReals.
      revert H ; apply hinhuniv ; apply sumofmaps ; intros H ;
        apply_pr2_in ispositive_multNonnegativeReals H ;
        apply maxNonnegativeReals_le ;
        apply_pr2 le0_NonnegativeReals.
      * now rewrite (hr_to_NRposneg_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals.
      * now rewrite (hr_to_NRposneg_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals.
      * now rewrite (hr_to_NRnegpos_zero _ (pr1 H)), islabsorb_zero_multNonnegativeReals.
      * now rewrite (hr_to_NRnegpos_zero _ (pr2 H)), israbsorb_zero_multNonnegativeReals.
  - intros H.
    apply_pr2_in ispositive_multNonnegativeReals H.
    rewrite hr_to_NRposneg_zero.
    + apply islabsorb_zero_multNonnegativeReals.
    + exact (pr1 H).
  - intros H.
    apply_pr2_in ispositive_multNonnegativeReals H.
    rewrite hr_to_NRposneg_zero.
    + apply islabsorb_zero_multNonnegativeReals.
    + exact (pr1 H).

Archimedean


Lemma nat_to_hr_O :
  nat_to_hr O = 0%ring.
Show proof.
  unfold nat_to_hr.
  rewrite nat_to_NonnegativeReals_O.
  reflexivity.

Lemma nat_to_hr_S :
  ∏ n : nat, nat_to_hr (S n) = (1 + nat_to_hr n)%ring.
Show proof.
  intros n.
  unfold nat_to_hr.
  rewrite nat_to_NonnegativeReals_Sn, iscomm_plusNonnegativeReals.
  rewrite <- (hr_to_NR_bij 1%ring), hr_to_NR_one, NR_to_hr_plus.
  rewrite !isrunit_zero_plusNonnegativeReals.
  reflexivity.

Lemma hr_archimedean :
  isarchCF (λ x y : hr_ConstructiveField, hr_lt_rel y x).
Show 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.

Completeness


Definition Cauchy_seq (u : nat → hr_ConstructiveField) : hProp.
Show proof.
  apply (make_hProp (∏ c : NonnegativeReals, 0 < c -> ∃ N : nat, ∏ n m : nat, N ≤ n -> N ≤ m -> hr_abs (u m - u n)%ring < c)).
  apply impred_isaprop ; intro.
  apply isapropimpl.
  apply pr2.

Lemma Cauchy_seq_pr1 (u : nat → hr_ConstructiveField) :
  let x := λ n : nat, hr_to_NRpos (u n) in
  Cauchy_seq u → NonnegativeReals.Cauchy_seq x.
Show proof.
  intros x.
  set (y := λ n : nat, hr_to_NRneg (u n)).
  assert (Hxy : ∏ n, NR_to_hr (x n ,, y n) = u n).
  { intros n.
    unfold x, y, hr_to_NRpos, hr_to_NRneg.
    apply hr_to_NR_bij. }
  intros Cu c Hc.
  generalize (Cu c Hc).
  apply hinhfun ; intros N.
  exists (pr1 N) ; intros n m Hn Hm.
  generalize ((pr2 N) _ _ Hn Hm) ; intros Hu.
  split.
  - apply (plusNonnegativeReals_ltcompat_r (x m)) in Hu.
    eapply istrans_le_lt_ltNonnegativeReals, Hu.
    rewrite hr_opp_minus, hr_abs_opp, ringcomm1.
    change (- - u n)%ring with (grinv hr_commring (grinv hr_commring (u n))).
    rewrite (grinvinv hr_commring (u n)).
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, maxNonnegativeReals_le_l.
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, hr_to_NRpos_minus.
    change (hr_to_NRpos (u n)) with (x n) ;
      change (hr_to_NRpos (u m)) with (x m).
    rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus.
    now apply maxNonnegativeReals_le_l.
  - apply (plusNonnegativeReals_ltcompat_r (x n)) in Hu.
    eapply istrans_le_lt_ltNonnegativeReals, Hu.
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, maxNonnegativeReals_le_l.
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, hr_to_NRpos_minus.
    change (hr_to_NRpos (u n)) with (x n) ;
      change (hr_to_NRpos (u m)) with (x m).
    rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus.
    now apply maxNonnegativeReals_le_l.
Lemma Cauchy_seq_pr2 (u : nat → hr_ConstructiveField) :
  let y := λ n : nat, hr_to_NRneg (u n) in
  Cauchy_seq u → NonnegativeReals.Cauchy_seq y.
Show proof.
  intros y.
  set (x := λ n : nat, hr_to_NRpos (u n)).
  assert (Hxy : ∏ n, NR_to_hr (x n ,, y n) = u n).
  { intros n.
    unfold x, y, hr_to_NRpos, hr_to_NRneg.
    apply hr_to_NR_bij. }
  intros Cu c Hc.
  generalize (Cu c Hc).
  apply hinhfun ; intros N.
  exists (pr1 N) ; intros n m Hn Hm.
  generalize ((pr2 N) _ _ Hn Hm) ; intros Hu.
  split.
  - apply (plusNonnegativeReals_ltcompat_r (y m)) in Hu.
    eapply istrans_le_lt_ltNonnegativeReals, Hu.
    rewrite hr_opp_minus, hr_abs_opp, ringcomm1.
    change (- - u n)%ring with (grinv hr_commring (grinv hr_commring (u n))).
    rewrite (grinvinv hr_commring (u n)).
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, maxNonnegativeReals_le_r.
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, hr_to_NRneg_minus.
    change (hr_to_NRneg (u n)) with (y n) ;
      change (hr_to_NRneg (u m)) with (y m).
    rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus.
    now apply maxNonnegativeReals_le_l.
  - apply (plusNonnegativeReals_ltcompat_r (y n)) in Hu.
    eapply istrans_le_lt_ltNonnegativeReals, Hu.
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, maxNonnegativeReals_le_r.
    eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, hr_to_NRneg_minus.
    change (hr_to_NRneg (u n)) with (y n) ;
      change (hr_to_NRneg (u m)) with (y m).
    rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus.
    now apply maxNonnegativeReals_le_l.

Definition is_lim_seq (u : nat → hr_ConstructiveField) (l : hr_ConstructiveField) : hProp.
Show proof.
  apply (make_hProp (∏ c : NonnegativeReals, 0 < c -> ∃ N : nat, ∏ n : nat, N ≤ n -> hr_abs (u n - l)%ring < c)).
  apply impred_isaprop ; intro.
  apply isapropimpl.
  apply pr2.
Definition ex_lim_seq (u : nat → hr_ConstructiveField) := ∑ l, is_lim_seq u l.

Lemma Cauchy_seq_impl_ex_lim_seq (u : nat → hr_ConstructiveField) :
  Cauchy_seq u → ex_lim_seq u.
Show proof.
  intros Cu.
  set (x := λ n, hr_to_NRpos (u n)).
  set (y := λ n, hr_to_NRneg (u n)).
  assert (Hxy : ∏ n, NR_to_hr (x n ,, y n) = u n).
  { intros n.
    unfold x, y, hr_to_NRpos, hr_to_NRneg.
    apply hr_to_NR_bij. }
  generalize (Cauchy_seq_impl_ex_lim_seq x (Cauchy_seq_pr1 u Cu)).
  set (lx := Cauchy_lim_seq x (Cauchy_seq_pr1 u Cu)) ; clearbody lx ; intro Hx.
  generalize (Cauchy_seq_impl_ex_lim_seq y (Cauchy_seq_pr2 u Cu)).
  set (ly := Cauchy_lim_seq y (Cauchy_seq_pr2 u Cu)) ; clearbody ly ; intro Hy.
  exists (NR_to_hr (lx,,ly)).
  intros c Hc.
  apply ispositive_halfNonnegativeReals in Hc.
  generalize (Hx _ Hc) (Hy _ Hc) ;
    apply hinhfun2 ; clear Hy Hx ;
    intros Nx Ny.
  exists (max (pr1 Nx) (pr1 Ny)) ; intros n Hn.
  rewrite <- Hxy ; simpl pr1.
  rewrite NR_to_hr_minus ; simpl.
  apply maxNonnegativeReals_lt.
  - rewrite hr_to_NRpos_NR_to_hr.
    apply_pr2 (plusNonnegativeReals_ltcompat_r (y n + lx)).
    rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus ; simpl.
    apply maxNonnegativeReals_lt.
    + rewrite (double_halfNonnegativeReals c), (iscomm_plusNonnegativeReals (y n)), (isassoc_plusNonnegativeReals lx (y n)), <- (isassoc_plusNonnegativeReals (y n)), (iscomm_plusNonnegativeReals (y n)), <- !isassoc_plusNonnegativeReals, (isassoc_plusNonnegativeReals (lx + _)).
      apply plusNonnegativeReals_ltcompat.
      * apply (pr2 Nx).
        apply istransnatleh with (2 := Hn).
        apply max_le_l.
      * apply_pr2 (pr2 Ny).
        apply istransnatleh with (2 := Hn).
        apply max_le_r.
    + apply plusNonnegativeReals_lt_r .
      now apply_pr2 ispositive_halfNonnegativeReals.
  - rewrite hr_to_NRneg_NR_to_hr.
    apply_pr2 (plusNonnegativeReals_ltcompat_r (x n + ly)).
    rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus ; simpl.
    apply maxNonnegativeReals_lt.
    + rewrite (double_halfNonnegativeReals c), (iscomm_plusNonnegativeReals (x n)), (isassoc_plusNonnegativeReals ly (x n)), <- (isassoc_plusNonnegativeReals (x n)), (iscomm_plusNonnegativeReals (x n)), <- !isassoc_plusNonnegativeReals, (isassoc_plusNonnegativeReals (ly + _)).
      apply plusNonnegativeReals_ltcompat.
      * apply (pr2 Ny).
        apply istransnatleh with (2 := Hn).
        apply max_le_r.
      * apply_pr2 (pr2 Nx).
        apply istransnatleh with (2 := Hn).
        apply max_le_l.
    + apply plusNonnegativeReals_lt_r .
      now apply_pr2 ispositive_halfNonnegativeReals.

Interface for Reals


Definition Reals : ConstructiveField := hr_ConstructiveField.

Operations and relations


Definition Rap : hrel Reals := CFap.
Definition Rlt : hrel Reals := hr_lt_rel.
Definition Rgt : hrel Reals := λ x y : Reals, Rlt y x.
Definition Rle : hrel Reals := hr_le_rel.
Definition Rge : hrel Reals := λ x y : Reals, Rle y x.

Definition Rzero : Reals := CFzero.
Definition Rplus : binop Reals := CFplus.
Definition Ropp : unop Reals := CFopp.
Definition Rminus : binop Reals := CFminus.

Definition Rone : Reals := CFone.
Definition Rmult : binop Reals := CFmult.
Definition Rinv : ∏ x : Reals, (Rap x Rzero) -> Reals := CFinv.
Definition Rdiv : Reals -> ∏ y : Reals, (Rap y Rzero) -> Reals := CFdiv.

Definition Rtwo : Reals := Rplus Rone Rone.
Definition Rabs : Reals → NonnegativeReals := hr_abs.

Definition NRNRtoR : NonnegativeReals → NonnegativeReals → Reals := λ (x y : NonnegativeReals), NR_to_hr (x,,y).
Definition RtoNRNR : Reals → NonnegativeReals × NonnegativeReals := λ x : Reals, (hr_to_NR x).

Declare Scope R_scope.
Delimit Scope R_scope with R.
Local Open Scope R_scope.

Infix "≠" := Rap : R_scope.
Infix "<" := Rlt : R_scope.
Infix ">" := Rgt : R_scope.
Infix "<=" := Rle : R_scope.
Infix ">=" := Rge : R_scope.

Notation "0" := Rzero : R_scope.
Notation "1" := Rone : R_scope.
Notation "2" := Rtwo : R_scope.
Infix "+" := Rplus : R_scope.
Notation "- x" := (Ropp x) : R_scope.
Infix "-" := Rminus : R_scope.
Infix "*" := Rmult : R_scope.
Notation "/ x" := (Rinv (pr1 x) (pr2 x)) : R_scope.
Notation "x / y" := (Rdiv x (pr1 y) (pr2 y)) : R_scope.

NRNRtoR and RtoNRNR


Lemma NRNRtoR_RtoNRNR :
  ∏ x : Reals, NRNRtoR (pr1 (RtoNRNR x)) (pr2 (RtoNRNR x)) = x.
Show proof.
  intros X.
  unfold NRNRtoR.
  apply hr_to_NR_bij.

Lemma RtoNRNR_NRNRtoR :
  ∏ x y : NonnegativeReals,
    (RtoNRNR (NRNRtoR x y)) = ((x - y)%NR ,, (y - x)%NR).
Show proof.
  intros X Y.
  unfold RtoNRNR, NRNRtoR.
  unfold hr_to_NR, NR_to_hr.
  now rewrite setquotunivcomm.

Lemma NRNRtoR_inside :
  ∏ x y : NonnegativeReals, pr1 (NRNRtoR x y) (x,,y).
Show proof.
  intros x y.
  apply hinhpr.
  exists 0%NR ; simpl.
  reflexivity.

Lemma NRNRtoR_zero :
  NRNRtoR 0%NR 0%NR = 0.
Show proof.
  unfold NRNRtoR, NR_to_hr.
  refine (setquotl0 _ 0 (_,,_)).
  apply hinhpr.
  exists 0%NR ; simpl.
  reflexivity.
Lemma NRNRtoR_one :
  NRNRtoR 1%NR 0%NR = 1.
Show proof.
  unfold NRNRtoR, NR_to_hr.
  refine (setquotl0 _ 1 (_,,_)).
  apply hinhpr.
  exists 0%NR ; simpl.
  reflexivity.

Lemma NRNRtoR_eq :
  ∏ x x' y y' : NonnegativeReals,
    (x + y' = x' + y)%NR <->
    NRNRtoR x y = NRNRtoR x' y'.
Show proof.
  intros x x' y y'.
  apply (NR_to_hr_eq (x,,y) (x' ,, y')).
Lemma NRNRtoR_ap :
  ∏ x x' y y' : NonnegativeReals,
    (x + y' ≠ x' + y)%NR <->
    NRNRtoR x y ≠ NRNRtoR x' y'.
Show proof.
  intros x x' y y'.
  apply (NR_to_hr_ap (x,,y) (x' ,, y')).
Lemma NRNRtoR_lt :
  ∏ x x' y y' : NonnegativeReals,
    (x + y' < x' + y)%NR <->
    NRNRtoR x y < NRNRtoR x' y'.
Show proof.
  intros x x' y y'.
  apply (NR_to_hr_lt (x,,y) (x' ,, y')).
Lemma NRNRtoR_le :
  ∏ x x' y y' : NonnegativeReals,
    (x + y' <= x' + y)%NR <->
    NRNRtoR x y <= NRNRtoR x' y'.
Show proof.
  intros x x' y y'.
  apply (NR_to_hr_le (x,,y) (x' ,, y')).

Lemma NRNRtoR_plus :
  ∏ x x' y y' : NonnegativeReals, NRNRtoR (x + x')%NR (y + y')%NR = NRNRtoR x y + NRNRtoR x' y'.
Show proof.
  intros x x' y y'.
  apply pathsinv0, NR_to_hr_plus.
Lemma NRNRtoR_opp :
  ∏ x y : NonnegativeReals, NRNRtoR y x = - NRNRtoR x y.
Show proof.
  intros x y.
  apply pathsinv0, NR_to_hr_opp.
Lemma NRNRtoR_minus :
  ∏ x x' y y' : NonnegativeReals, NRNRtoR (x + y')%NR (y + x')%NR = NRNRtoR x y - NRNRtoR x' y'.
Show proof.
  intros x x' y y'.
  apply pathsinv0, NR_to_hr_minus.
Lemma NRNRtoR_mult :
  ∏ x x' y y' : NonnegativeReals, NRNRtoR (x * x' + y * y')%NR (x * y' + y * x')%NR = NRNRtoR x y * NRNRtoR x' y'.
Show proof.
  intros x x' y y'.
  apply pathsinv0, NR_to_hr_mult.
Lemma NRNRtoR_inv_pos :
  ∏ (x : NonnegativeReals) Hrn Hr,
    NRNRtoR (invNonnegativeReals x Hrn) 0%NR = Rinv (NRNRtoR x 0%NR) Hr.
Show proof.
  intros x Hrn Hr.
  rewrite <- (isrunit_CFone_CFmult (NRNRtoR (invNonnegativeReals x Hrn) 0%NR)), <- (isrunit_CFone_CFmult (Rinv (NRNRtoR x 0%NR) Hr)).
  rewrite <- (isrinv_CFinv (X := Reals) (NRNRtoR x 0%NR) Hr).
  rewrite <- !(isassoc_CFmult (X := Reals)).
  apply (maponpaths (λ x, (x * _)%CF)).
  rewrite <- NRNRtoR_mult.
  unfold Rinv.
  rewrite (islinv_CFinv (X := Reals) (NRNRtoR x 0%NR) Hr).
  rewrite !israbsorb_zero_multNonnegativeReals, islabsorb_zero_multNonnegativeReals.
  rewrite !isrunit_zero_plusNonnegativeReals.
  rewrite islinv_invNonnegativeReals.
  apply NRNRtoR_one.
Lemma NRNRtoR_inv_neg :
  ∏ (x : NonnegativeReals) Hrn Hr,
    NRNRtoR 0%NR (invNonnegativeReals x Hrn) = Rinv (NRNRtoR 0%NR x) Hr.
Show proof.
  intros x Hrn Hr.
  rewrite <- (isrunit_CFone_CFmult (NRNRtoR 0%NR (invNonnegativeReals x Hrn))), <- (isrunit_CFone_CFmult (Rinv (NRNRtoR 0%NR x) Hr)).
  rewrite <- (isrinv_CFinv (X := Reals) (NRNRtoR 0%NR x) Hr).
  rewrite <- !(isassoc_CFmult (X := Reals)).
  apply (maponpaths (λ x, (x * _)%CF)).
  rewrite <- NRNRtoR_mult.
  unfold Rinv.
  rewrite (islinv_CFinv (X := Reals) (NRNRtoR 0%NR x) Hr).
  rewrite !israbsorb_zero_multNonnegativeReals, islabsorb_zero_multNonnegativeReals.
  rewrite !islunit_zero_plusNonnegativeReals.
  rewrite islinv_invNonnegativeReals.
  apply NRNRtoR_one.

Lemma Rabs_pr1RtoNRNR :
  ∏ x : Reals,
    (pr1 (RtoNRNR x) <= Rabs x)%NR.
Show proof.
  intros x.
  rewrite <- (NRNRtoR_RtoNRNR x).
  generalize (pr1 (RtoNRNR x)) (pr2 (RtoNRNR x)) ; clear x ; intros x y ; simpl.
  apply maxNonnegativeReals_le_l.
Lemma Rabs_pr2RtoNRNR :
  ∏ x : Reals,
    (pr2 (RtoNRNR x) <= Rabs x)%NR.
Show proof.
  intros x.
  rewrite <- (NRNRtoR_RtoNRNR x).
  generalize (pr1 (RtoNRNR x)) (pr2 (RtoNRNR x)) ; clear x ; intros x y ; simpl.
  apply maxNonnegativeReals_le_r.

Theorems about apartness and order


Lemma ispositive_Rone : 0 < 1.
Show proof.
  rewrite <- NRNRtoR_zero, <- NRNRtoR_one.
  apply NRNRtoR_lt.
  rewrite !isrunit_zero_plusNonnegativeReals.
  apply ispositive_apNonnegativeReals.
  apply isnonzeroNonnegativeReals.

Lemma isirrefl_Rlt :
  ∏ x : Reals, ¬ (x < x).
Show proof.
  exact (isirrefl_isStrongOrder (isStrongOrder_hr_lt)).
Lemma istrans_Rlt :
  ∏ x y z : Reals, x < y -> y < z -> x < z.
Show proof.
  exact (istrans_isStrongOrder (isStrongOrder_hr_lt)).
Lemma iscotrans_Rlt :
  ∏ (x y z : Reals), (x < z) -> (x < y) ∨ (y < z).
Show proof.
  exact iscotrans_hr_lt.

Lemma Rplus_ltcompat_l:
  ∏ x y z : Reals, y < z <-> (y + x) < (z + x).
Show proof.
  exact hr_plus_ltcompat_l.
Lemma Rplus_ltcompat_r:
  ∏ x y z : Reals, y < z <-> (x + y) < (x + z).
Show proof.
  exact hr_plus_ltcompat_r.
Lemma Rmult_ltcompat_l:
  ∏ x y z : Reals,
    0 < x -> y < z -> (y * x) < (z * x).
Show proof.
  exact hr_mult_ltcompat_l.
Lemma Rmult_ltcompat_l':
  ∏ x y z : Reals,
    0 <= x -> (y * x) < (z * x) -> y < z.
Show proof.
  exact hr_mult_ltcompat_l'.
Lemma Rmult_ltcompat_r:
  ∏ x y z : Reals,
    0 < x -> y < z -> (x * y) < (x * z).
Show proof.
  intros x y z.
  rewrite !(iscomm_CFmult x).
  now apply Rmult_ltcompat_l.
Lemma Rmult_ltcompat_r':
  ∏ x y z : Reals,
    0 <= x -> (x * y) < (x * z) -> y < z.
Show proof.
  exact hr_mult_ltcompat_r'.

Lemma Rarchimedean:
  ∏ x : Reals, ∃ n : nat, x < nattoring n.
Show proof.
  exact hr_archimedean.

Lemma notRlt_Rle :
  ∏ x y : Reals, ¬ (x < y) <-> (y <= x).
Show proof.
  exact hr_notlt_le.
Lemma Rlt_Rle :
  ∏ x y : Reals, x < y -> x <= y.
Show proof.
  intros x y H.
  apply notRlt_Rle.
  intros H0.
  refine (isirrefl_Rlt _ _).
  refine (istrans_Rlt _ _ _ _ _).
  - exact H.
  - exact H0.
Lemma isantisymm_Rle :
  ∏ x y : Reals, x <= y -> y <= x -> x = y.
Show proof.
  exact isantisymm_hr_le.
Lemma istrans_Rle :
  ∏ x y z : Reals, x <= y -> y <= z -> x <= z.
Show proof.
  intros x y z Hxy Hyz.
  apply notRlt_Rle ; intro H.
  generalize (iscotrans_Rlt _ y _ H).
  apply factor_through_squash.
  { exact isapropempty. }
  apply sumofmaps.
  + apply_pr2 notRlt_Rle.
    exact Hyz.
  + apply_pr2 notRlt_Rle.
    exact Hxy.
Lemma istrans_Rle_lt :
  ∏ x y z : Reals, x <= y -> y < z -> x < z.
Show proof.
  intros x y z Hxy Hyz.
  generalize (iscotrans_Rlt _ x _ Hyz).
  apply hinhuniv.
  apply sumofmaps ; intros H.
  - apply fromempty.
    revert H.
    apply_pr2 notRlt_Rle.
    exact Hxy.
  - exact H.
Lemma istrans_Rlt_le :
  ∏ x y z : Reals, x < y -> y <= z -> x < z.
Show proof.
  intros x y z Hxy Hyz.
  generalize (iscotrans_Rlt _ z _ Hxy).
  apply hinhuniv.
  apply sumofmaps ; intros H.
  - exact H.
  - apply fromempty.
    revert H.
    apply_pr2 notRlt_Rle.
    exact Hyz.

Lemma Rplus_lecompat_l:
  ∏ x y z : Reals, y <= z <-> (y + x) <= (z + x).
Show proof.
  exact hr_plus_lecompat_l.
Lemma Rplus_lecompat_r:
  ∏ x y z : Reals, y <= z <-> (x + y) <= (x + z).
Show proof.
  exact hr_plus_lecompat_r.
Lemma Rmult_lecompat_l:
  ∏ x y z : Reals,
    0 <= x -> y <= z -> (y * x) <= (z * x).
Show proof.
  exact hr_mult_lecompat_l.
Lemma Rmult_lecompat_l':
  ∏ x y z : Reals,
    0 < x -> (y * x) <= (z * x) -> y <= z.
Show proof.
  exact hr_mult_lecompat_l'.
Lemma Rmult_lecompat_r:
  ∏ x y z : Reals,
    0 <= x -> y <= z -> (x * y) <= (x * z).
Show proof.
  exact hr_mult_lecompat_r.
Lemma Rmult_lecompat_r':
  ∏ x y z : Reals,
    0 < x -> (x * y) <= (x * z) -> y <= z.
Show proof.
  exact hr_mult_lecompat_r'.

Lemma Rap_Rlt:
  ∏ x y : Reals, x ≠ y <-> (x < y) ⨿ (y < x).
Show proof.
  exact hr_ap_lt.

Lemma isnonzeroReals : (1 ≠ 0).
Show proof.
  exact isnonzeroCF.

Lemma isirrefl_Rap :
  ∏ x : Reals, ¬ (x ≠ x).
Show proof.
  exact isirrefl_CFap.
Lemma issymm_Rap :
  ∏ (x y : Reals), (x ≠ y) -> (y ≠ x).
Show proof.
  exact issymm_CFap.
Lemma iscotrans_Rap :
  ∏ (x y z : Reals), (x ≠ z) -> (x ≠ y) ∨ (y ≠ z).
Show proof.
  exact iscotrans_CFap.
Lemma istight_Rap :
  ∏ (x y : Reals), ¬ (x ≠ y) -> x = y.
Show proof.
  exact istight_CFap.

Lemma apRplus :
  ∏ (x x' y y' : Reals),
    (x + y ≠ x' + y') -> (x ≠ x') ∨ (y ≠ y').
Show proof.
  exact apCFplus.
Lemma Rplus_apcompat_l :
  ∏ x y z : Reals,
    y + x ≠ z + x <-> y ≠ z.
Show proof.
  exact CFplus_apcompat_l.
Lemma Rplus_apcompat_r :
  ∏ x y z : Reals,
    x + y ≠ x + z <-> y ≠ z.
Show proof.
  exact CFplus_apcompat_r.

Lemma apRmult:
  ∏ (x x' y y' : Reals),
  (x * y ≠ x' * y') -> (x ≠ x') ∨ (y ≠ y').
Show proof.
  apply apCFmult.
Lemma Rmult_apcompat_l:
  ∏ (x y z : Reals), (y * x ≠ z * x) -> (y ≠ z).
Show proof.
  exact CFmult_apcompat_l.
Lemma Rmult_apcompat_l':
  ∏ (x y z : Reals),
    (x ≠ 0) -> (y ≠ z) -> (y * x ≠ z * x).
Show proof.
  exact CFmult_apcompat_l'.
Lemma Rmult_apcompat_r:
  ∏ (x y z : Reals), (x * y ≠ x * z) -> (y ≠ z).
Show proof.
  exact CFmult_apcompat_r.
Lemma Rmult_apcompat_r':
  ∏ (x y z : Reals),
    (x ≠ 0) -> (y ≠ z) -> (x * y ≠ x * z).
Show proof.
  exact CFmult_apcompat_r'.
Lemma RmultapRzero:
  ∏ (x y : Reals),
    (x * y ≠ 0) -> (x ≠ 0) ∧ (y ≠ 0).
Show proof.
  exact CFmultapCFzero.

Algrebra


Lemma islunit_Rzero_Rplus :
  ∏ x : Reals, 0 + x = x.
Show proof.
  exact islunit_CFzero_CFplus.
Lemma isrunit_Rzero_Rplus :
  ∏ x : Reals, x + 0 = x.
Show proof.
  exact isrunit_CFzero_CFplus.
Lemma isassoc_Rplus :
  ∏ x y z : Reals, x + y + z = x + (y + z).
Show proof.
  exact isassoc_CFplus.
Lemma islinv_Ropp :
  ∏ x : Reals, - x + x = 0.
Show proof.
  exact islinv_CFopp.
Lemma isrinv_Ropp :
  ∏ x : Reals, x + - x = 0.
Show proof.
  exact isrinv_CFopp.

Lemma iscomm_Rplus :
  ∏ x y : Reals, x + y = y + x.
Show proof.
  exact iscomm_CFplus.
Lemma islunit_Rone_Rmult :
  ∏ x : Reals, 1 * x = x.
Show proof.
  exact islunit_CFone_CFmult.
Lemma isrunit_Rone_Rmult :
  ∏ x : Reals, x * 1 = x.
Show proof.
  exact isrunit_CFone_CFmult.
Lemma isassoc_Rmult :
  ∏ x y z : Reals, x * y * z = x * (y * z).
Show proof.
  exact isassoc_CFmult.
Lemma iscomm_Rmult :
  ∏ x y : Reals, x * y = y * x.
Show proof.
  exact iscomm_CFmult.
Lemma islinv_Rinv :
  ∏ (x : Reals) (Hx0 : x ≠ 0),
    (Rinv x Hx0) * x = 1.
Show proof.
  exact islinv_CFinv.
Lemma isrinv_Rinv :
  ∏ (x : Reals) (Hx0 : x ≠ 0),
    x * (Rinv x Hx0) = 1.
Show proof.
  exact isrinv_CFinv.
Lemma islabsorb_Rzero_Rmult :
  ∏ x : Reals, 0 * x = 0.
Show proof.
  exact islabsorb_CFzero_CFmult.
Lemma israbsorb_Rzero_Rmult :
  ∏ x : Reals, x * 0 = 0.
Show proof.
  exact israbsorb_CFzero_CFmult.
Lemma isldistr_Rplus_Rmult :
  ∏ x y z : Reals, z * (x + y) = z * x + z * y.
Show proof.
  exact isldistr_CFplus_CFmult.
Lemma isrdistr_Rplus_Rmult :
  ∏ x y z : Reals, (x + y) * z = x * z + y * z.
Show proof.
  exact isrdistr_CFplus_CFmult.

Rabs


Lemma istriangle_Rabs :
  ∏ x y : Reals, (Rabs (x + y)%R <= Rabs x + Rabs y)%NR.
Show proof.
  exact istriangle_hr_abs.
Lemma istriangle_Rabs' :
  ∏ x y : Reals, (Rabs x - Rabs y <= Rabs (x + y)%R)%NR.
Show proof.
  exact istriangle_hr_abs'.

Lemma Rabs_Rmult :
  ∏ x y : Reals, (Rabs (x * y)%R = Rabs x * Rabs y)%NR.
Show proof.
  exact hr_abs_mult.

Lemma Rabs_Ropp :
  ∏ x : Reals, (Rabs (- x)%R = Rabs x).
Show proof.
  intros x.
  rewrite <- (NRNRtoR_RtoNRNR x).
  apply iscomm_maxNonnegativeReals.