Library UniMath.RealNumbers.Prelim

Additional theorems and definitions


Require Import UniMath.Foundations.Preamble.
Require Import UniMath.MoreFoundations.Tactics.

Require Export UniMath.Topology.Prelim.

for RationalNumbers.v


Require Export UniMath.NumberSystems.RationalNumbers.
Require Export UniMath.Algebra.Archimedean.

Local Open Scope hq_scope.

Notation "x <= y" := (hqleh x y) : hq_scope.
Notation "x >= y" := (hqgeh x y) : hq_scope.
Notation "x < y" := (hqlth x y) : hq_scope.
Notation "x > y" := (hqgth x y) : hq_scope.
Notation "/ x" := (hqmultinv x) : hq_scope.
Notation "x / y" := (hqdiv x y) : hq_scope.
Notation "2" := (hztohq (nattohz 2)) : hq_scope.

Lemma hzone_neg_hzzero : neg (1%hz = 0%hz).
Show proof.
  confirm_not_equal isdeceqhz.

Definition one_intdomnonzerosubmonoid : intdomnonzerosubmonoid hzintdom.
Show proof.
  exists 1%hz ; simpl.
  exact hzone_neg_hzzero.

Opaque hz.

Lemma hq2eq1plus1 : 2 = 1 + 1.
Show proof.
  confirm_equal isdeceqhq.

Lemma hq2_gt0 : 2 > 0.
Show proof.
  confirm_yes hqgthdec 2 0.

Lemma hq1_gt0 : 1 > 0.
Show proof.
  confirm_yes hqgthdec 1 0.

Lemma hq1ge0 : (0 <= 1)%hq.
Show proof.
  confirm_yes hqlehdec 0 1.

Lemma hqgth_hqneq :
  ∏ x y : hq, x > y -> hqneq x y.
Show proof.
  intros x y Hlt Heq.
  rewrite Heq in Hlt.
  now apply isirreflhqgth with y.

Lemma hqldistr :
  ∏ x y z, x * (y + z) = x * y + x * z.
Show proof.
  intros x y z.
  now apply ringldistr.

Lemma hqmult2r :
  ∏ x : hq, x * 2 = x + x.
Show proof.
  intros x.
  now rewrite hq2eq1plus1, hqldistr, (hqmultr1 x).

Lemma hqplusdiv2 : ∏ x : hq, x = (x + x) / 2.
  intros x.
  apply hqmultrcan with 2.
  - now apply hqgth_hqneq, hq2_gt0.
  - unfold hqdiv.
    rewrite hqmultassoc.
    rewrite (hqislinvmultinv 2).
    2: now apply hqgth_hqneq, hq2_gt0.
    rewrite (hqmultr1 (x + x)).
    apply hqmult2r.
Qed.

Lemma hqlth_between :
  ∏ x y : hq, x < y -> total2 (λ z, (x < z) × (z < y)).
Show proof.
  assert (H0 : / 2 > 0).
  { apply hqgthandmultlinv with 2.
    - apply hq2_gt0.
    - rewrite hqisrinvmultinv, hqmultx0.
      + now apply hq1_gt0.
      + now apply hqgth_hqneq, hq2_gt0.
  }
  intros x y Hlt.
  exists ((x + y) / 2).
  split.
  - pattern x at 1.
    rewrite (hqplusdiv2 x).
    unfold hqdiv.
    apply (hqlthandmultr _ _ (/ 2)).
    + exact H0.
    + now apply (hqlthandplusl _ _ x Hlt).
  - pattern y at 2.
    rewrite (hqplusdiv2 y).
    unfold hqdiv.
    apply (hqlthandmultr _ _ (/ 2)).
    + exact H0.
    + now apply (hqlthandplusr _ _ y Hlt).

Lemma hq0lehandplus:
  ∏ n m : hq,
    0 <= n -> 0 <= m -> 0 <= (n + m).
Show proof.
  intros n m Hn Hm.
  eapply istranshqleh, hqlehandplusl, Hm.
  now rewrite hqplusr0.

Lemma hq0lehandmult:
  ∏ n m : hq, 0 <= n -> 0 <= m -> 0 <= n * m.
Show proof.
  intros n m.
  exact hqmultgeh0geh0.

Lemma hq0leminus :
  ∏ r q : hq, r <= q -> 0 <= q - r.
Show proof.
  intros r q Hr.
  apply hqlehandplusrinv with r.
  unfold hqminus.
  rewrite hqplusassoc, hqlminus.
  now rewrite hqplusl0, hqplusr0.

Lemma hqinv_gt0 (x : hq) : 0 < x → 0 < / x.
Show proof.
  unfold hqlth.
  intros Hx.
  apply hqgthandmultlinv with x.
  - exact Hx.
  - rewrite hqmultx0.
    rewrite hqisrinvmultinv.
    + exact hq1_gt0.
    + apply hqgth_hqneq.
      exact Hx.

Lemma hztohqandleh':
  ∏ n m : hz, (hztohq n <= hztohq m)%hq → hzleh n m.
Show proof.
  intros n m Hle Hlt.
  simple refine (Hle _).
  apply hztohqandgth.
  exact Hlt.
Lemma hztohqandlth':
  ∏ n m : hz, (hztohq n < hztohq m)%hq -> hzlth n m.
Show proof.
  intros n m Hlt.
  apply neghzgehtolth.
  intro Hle.
  apply hztohqandgeh in Hle.
  apply hqgehtoneghqlth in Hle.
  apply Hle.
  exact Hlt.

Close Scope hq_scope.