# Library UniMath.RealNumbers.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).
Proof.
confirm_not_equal isdeceqhz.
Qed.

Definition one_intdomnonzerosubmonoid : intdomnonzerosubmonoid hzintdom.
Proof.
1%hz ; simpl.
exact hzone_neg_hzzero.
Defined.

Opaque hz.

Lemma hq2eq1plus1 : 2 = 1 + 1.
Proof.
confirm_equal isdeceqhq.
Qed.

Lemma hq2_gt0 : 2 > 0.
Proof.
confirm_yes hqgthdec 2 0.
Qed.

Lemma hq1_gt0 : 1 > 0.
Proof.
confirm_yes hqgthdec 1 0.
Qed.

Lemma hq1ge0 : (0 1)%hq.
Proof.
confirm_yes hqlehdec 0 1.
Qed.

Lemma hqgth_hqneq :
x y : hq, x > y hqneq x y.
Proof.
intros x y Hlt Heq.
rewrite Heq in Hlt.
now apply isirreflhqgth with y.
Qed.

Lemma hqldistr :
x y z, x × (y + z) = x × y + x × z.
Proof.
intros x y z.
now apply ringldistr.
Qed.

Lemma hqmult2r :
x : hq, x × 2 = x + x.
Proof.
intros x.
now rewrite hq2eq1plus1, hqldistr, (hqmultr1 x).
Qed.

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)).
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.
((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).
Qed.

Lemma hq0lehandplus:
n m : hq,
0 n 0 m 0 (n + m).
Proof.
intros n m Hn Hm.
eapply istranshqleh, hqlehandplusl, Hm.
now rewrite hqplusr0.
Qed.

Lemma hq0lehandmult:
n m : hq, 0 n 0 m 0 n × m.
Proof.
intros n m.
exact hqmultgeh0geh0.
Qed.

Lemma hq0leminus :
r q : hq, r q 0 q - r.
Proof.
intros r q Hr.
apply hqlehandplusrinv with r.
unfold hqminus.
rewrite hqplusassoc, hqlminus.
now rewrite hqplusl0, hqplusr0.
Qed.

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

Lemma hztohqandleh':
n m : hz, (hztohq n hztohq m)%hq hzleh n m.
Proof.
intros n m Hle Hlt.
simple refine (Hle _).
apply hztohqandgth.
exact Hlt.
Qed.
Lemma hztohqandlth':
n m : hz, (hztohq n < hztohq m)%hq hzlth n m.
Proof.
intros n m Hlt.
apply neghzgehtolth.
intro Hle.
apply hztohqandgeh in Hle.
apply hqgehtoneghqlth in Hle.
apply Hle.
exact Hlt.
Qed.

Close Scope hq_scope.