Require Import logical.
Require Import algebra.
Require Import naturals.
Require Import fractions.

(** * Positive Rational Numbers *)

(** ** Rational Numbers as sets of fractions represented by a canonical member [red x] *)

(** We consider a certain fraction [x]. The set [num_set x] contains all 
natural numbers n with the following property: [exists m. n/m ~ x].*)

Definition equiv (x:frac) (y1:nat) (y2:nat) := y1/y2 ~~ x.

Definition getDen (x:frac) (y1:nat) := first (equiv x y1) (mul_nat y1 (den x)).

Definition p_set (x:frac) (y1:nat) := equiv x y1 (getDen x y1). 

Lemma num_set_equiv_a (x:frac) (y1:nat) : p_set x y1 -> exists y2, equiv x y1 y2.
intros x y1 A.
exists (first (equiv x y1) (mul_nat y1 (den x))).
apply A.
Qed.

Lemma num_set_equiv_b (x:frac) (y1:nat) : (exists y2, equiv x y1 y2) -> p_set x y1.
intros [x1 x2] y1 [y2 A].
unfold equiv,p_set in *.
generalize (frac_order_equiv_b A); intros B.
unfold eq_frac_prop in B. simpl.
generalize (first_correct_b (equiv (x1/x2) y1) y2 (mul_nat y1 x2)).
intros C. apply C.
rewrite B,satz29.
apply leq_nat_mul_const.
apply A.
Qed.

Lemma num_set_equiv_c (x y:frac) (n:nat) : x ~ y -> p_set x n -> p_set y n.
intros x y n A B.
destruct (num_set_equiv_a _ _ B) as [m C].
unfold equiv in *.
apply num_set_equiv_b.
exists m.
apply (frac_order_equiv_a (satz39 _ _ _ (frac_order_equiv_b C) A)).
Qed.

(** Given a fraction [x] the function [red] takes the least member of [num_set x]
as the numerator for the reduced fraction. The denominator is easily computational
from that point. *)

Definition red (x:frac) := match x with x1/x2 =>
let i := first (p_set x) x1
in 
i / getDen x i
end.

Lemma red_a {x1 x2:nat} : p_set (x1/x2) x1.
intros x1 x2; unfold p_set. simpl.
apply (first_correct_b (equiv (x1/x2) x1) x2 (mul_nat x1 x2)).
rewrite satz29; apply leq_nat_mul_const.
apply frac_order_equiv_a, satz37.
Qed.

Lemma red_b {x y:frac} : x~y -> forall n, p_set x n = p_set y n.
intros x y A n.
apply pe_bool. split.
apply (num_set_equiv_c _ _ _ A).
apply (num_set_equiv_c _ _ _ (satz38 _ _ A)).
Qed.

Lemma redAx2 (x:frac) : x ~ red x.
intros [x1 x2]. apply satz38.
apply frac_order_equiv_b.
apply (firstMember _ (@red_a x1 x2)).
Qed.

Lemma redAx1 (x y:frac) : x ~ y -> red x = red y.
intros [x1 x2] [y1 y2] A.
apply frac_equal_num.
apply (satz39 _ _ _  (satz38 _ _ (redAx2 _)) (satz39 _ _ _  A (redAx2 _))).
simpl.
destruct (satz10H0 x1 y1) as [B|[B|B]].
rewrite (@firstConstant' (p_set (x1/x2)) _ (red_a) y1 B).
apply (first_correct_c _ _ (red_b A)).
subst x1.
apply (first_correct_c _ _ (red_b A)).
rewrite (@firstConstant' (p_set (y1/y2)) _ (red_a) x1 B).
apply (first_correct_c _ _ (red_b A)).
Qed.

Lemma redAx1_rev (x y:frac) : red x = red y -> x~y.
intros x y A.
apply (satz39 _ _ _  (redAx2 x) (satz39 _ _ _  (eq_frac_lemma A) (satz38 _ _ (redAx2 y)))).
Qed.

Lemma red_equiv_a (x y:frac) : red x ~ red y -> x ~ y.
intros x y A.
apply (satz39 _ _ _  (redAx2 _) (satz39 _ _ _  A (satz38 _ _ (redAx2 _)))).
Qed.

Lemma red_equiv_b {x y:frac} : x ~ y -> red x ~ red y.
intros x y A. rewrite (redAx1 _ _ A).
apply satz37.
Qed.

Definition fred (x:frac) : bool := equal_frac x (red x).

Lemma red_idemp {x:frac} : red x = red (red x).
intros x.
rewrite<- (redAx1 _ _ (redAx2 x)).
reflexivity.
Qed.

Lemma red_reduced : forall x, fred (red x).
intros x. unfold fred.
apply eq_frac_equiv_a.
exact red_idemp.
Qed.

(** * Definition of the Positive Rational Numbers *)

Record prat : Type := Prat
   {rep : frac;
    redp : fred rep}.

Theorem satz78 {x:prat} : x=x.
reflexivity.
Qed.

Theorem satz79 {x y:prat} : x=y -> y=x.
symmetry. exact H.
Qed.

Theorem satz80 {x y z:prat} : x=y -> y=z -> x=z.
intros x y z. transitivity y; tauto.
Qed.

Definition eq_prat_a (x y:prat) := rep x = rep y.

Lemma eq_prat_equiv_a {x y:prat} : x=y -> eq_prat_a x y.
intros x y A. rewrite A.
reflexivity.
Qed.

Lemma eq_prat_equiv_b {x y:prat} : eq_prat_a x y -> x=y.
intros [xr xp] [yr yp]. unfold eq_prat_a. simpl. intros A.
subst xr.
rewrite (pi_bool _ xp yp).
reflexivity.
Qed.


(** Order of positive rationals *)

Definition lt_prat (x y:prat) := rep x < rep y.
Notation "x < y":=(lt_prat x y).

Definition leq_prat (x y:prat) := rep x <~ rep y.
Notation "x <= y":=(leq_prat x y).

Definition eq_prat_b (x y:prat) := rep x ~ rep y.
Notation "x == y":=(eq_prat_b x y).

Lemma eq_prat_equiv_c {x y:prat} : eq_prat_a x y -> eq_prat_b x y.
intros x y A. unfold eq_prat_b. rewrite A.
apply satz37.
Qed.

Lemma eq_prat_equiv_d {x y:prat} : eq_prat_b x y -> eq_prat_a x y.
intros [xr xp] [yr yp]. unfold eq_prat_a. simpl.
unfold eq_prat_b. simpl. intros A.
unfold fred in xp.
rewrite (eq_frac_equiv_b xp).
rewrite (eq_frac_equiv_b yp).
apply (redAx1 _ _ A).
Qed.

Lemma eq_prat_equiv_e {x y:prat} : x=y -> x==y.
intros x y A.
exact (eq_prat_equiv_c (eq_prat_equiv_a A)).
Qed.

Lemma eq_prat_equiv_f {x y:prat} : x==y -> x=y.
intros x y A.
exact (eq_prat_equiv_b (eq_prat_equiv_d A)).
Qed.

Lemma leq_prat_reflexive : reflexive prat leq_prat.
intros [[x1 x2] xrp]. unfold leq_prat. simpl.
apply leq_frac_reflexive.
Qed.

Lemma leq_prat_linear : linear prat leq_prat.
intros x y. unfold leq_prat. destruct (@satz41H0 (rep y) (rep x)) as [A|[A|A]].
right. apply frac_order_equiv_d. right. apply A.
left. apply frac_order_equiv_d. left. apply (satz38 _ _  A).
left. apply frac_order_equiv_d. right. apply A.
Qed.

Theorem satz81H0 : trichotomy prat lt_prat.
intros x y. 
generalize (satz41H0 (rep x) (rep y)); intros [A|[A|A]].
left. exact A.
right. left. apply (eq_prat_equiv_f A).
right. right. exact A.
Qed.

Theorem satz81H1 {x y:prat} : y<x -> x=y -> False.
intros x y A B. apply (satz41H1 _ _ A (eq_prat_equiv_e B)).
Qed.

Theorem satz81H2 {x y:prat} : y<x -> x<y -> False.
intros x y. apply satz41H2.
Qed.

Theorem satz81H3 {x y:prat} : x<y -> x=y -> False.
intros x y A B. apply (satz41H3 _ _ A (eq_prat_equiv_e B)).
Qed.

Theorem satz86 : transitive prat lt_prat.
intros x y z. apply satz50.
Qed.

Theorem lt_prat_irreflexive : irreflexive prat lt_prat.
intros x. apply lt_frac_irreflexive.
Qed.

(* leq_prat_transitive *)
Theorem satz88 : transitive prat leq_prat.
intros x y z. apply satz52a.
Qed.

Theorem leq_prat_antisymmetric : antisymmetric prat leq_prat.
intros x y A B.
destruct (frac_order_equiv_c A) as [C|C]; destruct (frac_order_equiv_c B) as [D|D].
apply eq_prat_equiv_f. apply (satz38 _ _  D).
contradiction (satz81H1 D (eq_prat_equiv_f C)).
contradiction (satz81H1 C (eq_prat_equiv_f D)).
contradiction (satz81H2 C D).
Qed.

Coercion frac_to_prat (x:frac) := Prat (red x) (red_reduced x).

Lemma frac_to_prat_resp_lt (x y:frac) : lt_frac x y -> x < y.
intros x y A. unfold lt_prat.
unfold frac_to_prat. simpl.
apply (satz44 A (redAx2 _) (redAx2 _)).
Qed.

Theorem satz89 {x:prat} : exists y, x<y.
intros x. destruct (@satz53 (rep x)).
exists x0.
exact (satz44 H (satz37 _) (redAx2 _)).
Qed.

Theorem satz90 {x:prat} : exists y, y<x.
intros x. destruct (@satz54 (rep x)) as [u A].
exists u.
exact (satz44 A (redAx2 _) (satz37 _)).
Qed.

Theorem satz91 {x y:prat} : x<y -> exists z, x<z /\ z<y.
intros x y A. destruct (@satz55 (rep x) (rep y) A) as [u [B C]].
exists u.
split.
exact (satz44 B (satz37 _) (redAx2 _)).
exact (satz44 C (redAx2 _) (satz37 _)).
Qed.

Definition add_prat (x y:prat):prat := rep x + rep y.
Notation "x + y":=(add_prat x y).

(* add_prat_commutative *)
Theorem satz92 : commutative prat add_prat.
intros [xr xp] [yr yp].
apply eq_prat_equiv_b.
unfold eq_prat_a. simpl.
apply redAx1.
apply satz58.
Qed.

(* add_prat_associative *)
Theorem satz93 : associative prat add_prat.
intros [xr xp] [yr yp] [zr zp].
unfold add_prat.
apply eq_prat_equiv_b. unfold eq_prat_a. simpl.
apply redAx1.
apply (satz39 _ _ _  (satz39 _ _ _  (satz56 (satz38 _ _  (redAx2 (add_frac xr yr))) (satz37 zr)) satz59) 
              (satz56 (satz37 xr) (redAx2 (add_frac yr zr)))).
Qed.

Theorem satz94 {x y:prat} : x < x+y.
intros x y.
unfold lt_prat. simpl.
apply (satz44 satz60 (satz37 _) (redAx2 _)).
Qed.

Theorem satz95 {x y z:prat} : x<y -> x+z < y+z.
intros x y z A.
unfold lt_prat. simpl.
apply (satz44 (satz61 _ _ _ A) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz96 {x y z:prat} : x=y -> x+z = y+z.
intros x y z A.
apply eq_prat_equiv_b. unfold eq_prat_a.
simpl. apply redAx1.
apply (satz62b (eq_prat_equiv_e A)).
Qed.

Theorem satz97a {x y z:prat} : x+z < y+z -> x<y.
intros x y z. unfold lt_prat. simpl.
intros A.
apply (satz63a (satz44 A (satz38 _ _  (redAx2 _)) (satz38 _ _  (redAx2 _)))).
Qed.

Theorem satz97b {x y z:prat} : x+z = y+z -> x=y.
intros x y z A.
generalize (eq_prat_equiv_a A); intros B.
apply eq_prat_equiv_f. unfold eq_prat_b.
unfold eq_prat_a in B. simpl in B.
apply (satz63b (redAx1_rev _ _ B)).
Qed.

Theorem satz98 {x y z u:prat} : x<y -> z<u -> x+z<y+u.
intros x y z u. unfold lt_prat. simpl.
intros A B. apply (satz44 (satz64 A B) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz99a {x y z u:prat} : x<=y -> z<u -> x+z<y+u.
intros x y z u A B.
apply (satz44 (satz65a A B) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz99b {x y z u:prat} : x<y -> z<=u -> x+z<y+u.
intros x y z u A B.
apply (satz44 (satz65b A B) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz100 {x y z u:prat} : x<=y -> z<=u -> x+z<=y+u.
intros x y z u A B.
generalize (satz66a A B); intros C. apply frac_order_equiv_d.
destruct (frac_order_equiv_c C) as [D|D].
left. apply eq_prat_equiv_c. unfold add_prat. unfold eq_prat_a. 
simpl. apply (redAx1 _ _ D).
right. apply (satz44 D (redAx2 _) (redAx2 _)).
Qed.

Theorem satz101a {x y:prat} : y<x -> exists z, y+z=x.
intros x y A.
generalize (satz67a A); intros [u B].
exists u. 
apply eq_prat_equiv_f. unfold eq_prat_b. simpl.
apply (satz39 _ _ _  (satz39 _ _ _  (satz38 _ _  (redAx2 _)) 
              (satz56 (satz37 _) (satz38 _ _  (redAx2 _)))) B).
Qed.

Theorem satz101b {x y u w:prat} : u+y=x -> w+y=x -> u=w.
intros x y u w. unfold add_prat.
intros A B.
apply (eq_prat_equiv_f (satz67b (satz39 _ _ _  (redAx2 _) (eq_prat_equiv_e A))
 (satz39 _ _ _  (redAx2 _) (eq_prat_equiv_e B)))).
Qed.

Theorem satz101c {x y:prat} : x<=y -> forall z, y+z=x -> False.
intros x y A z B.
rewrite<- B in A.
destruct (frac_order_equiv_c A) as [C|C].
apply (satz81H1 satz94 (eq_prat_equiv_f C)).
apply (satz81H2 (satz94) C).
Qed.

(** Subtraction of Prats *)
Definition sub_prat (x y:prat) (l:y<x) :prat := sub_frac (rep x) (rep y) l.

Theorem sub_prat_correct_a (x y:prat) (l: x < y) : x + (sub_prat y x l) = y.
intros [[x1 x2] xrp] [[y1 y2] yrp] A; symmetry.
apply eq_prat_equiv_f. unfold eq_prat_b.
unfold add_prat. unfold sub_prat. unfold frac_to_prat. unfold rep.
apply (@satz39 _ (add_frac (x1/x2) (red (sub_frac (y1/y2) (x1/x2) A)))).
unfold lt_prat in A. simpl in A.
apply (satz39 _ _ _  (sub_frac_correct_a _ _ A)).
apply (satz56 (satz37 _) (redAx2 _)).
apply redAx2.
Qed.

(** Multiplication of Prats *)

Definition mul_prat (x y:prat):prat := rep x * rep y.
Notation "x * y":=(mul_prat x y).

(* mul_prat_commutative *)
Theorem satz102 : commutative prat mul_prat.
intros x y. unfold mul_prat. apply eq_prat_equiv_b.
unfold eq_prat_a. simpl. apply redAx1.
apply satz69.
Qed.

(* mul_prat_associative *)
Theorem satz103 : associative prat mul_prat.
intros x y z. unfold mul_prat. apply eq_prat_equiv_b.
unfold eq_prat_a. simpl. apply redAx1.
apply (satz39 _ _ _  (satz39 _ _ _  (satz68 (satz38 _ _  (redAx2 _)) (satz37 _)) satz70)
   (satz68 (satz37 _) (redAx2 _))).
Qed.

(* add_prat_mul_prat_distributes *)
Theorem satz104 : distributes prat add_prat mul_prat.
intros x y z. unfold add_prat. unfold mul_prat. simpl.
apply eq_prat_equiv_b. unfold eq_prat_a. simpl.
apply redAx1.
apply (satz39 _ _ _  (satz39 _ _ _  (satz68 (satz37 _) (satz38 _ _  (redAx2 _))) satz71)
   (satz56 (redAx2 _) (redAx2 _))).
Qed.

Theorem satz105a {x y z:prat} : x<y -> x*z<y*z.
intros x y z A.
unfold lt_prat. unfold mul_prat. simpl.
apply (satz44 (satz72a _ _ _ A) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz105b {x y z:prat} : x=y -> x*z=y*z.
intros x y z A. apply eq_prat_equiv_b.
unfold eq_prat_a. simpl.
apply redAx1.
apply (satz72b _ _ _ (eq_prat_equiv_e A)).
Qed.

Theorem satz106a {x y z:prat} : x*z<y*z -> x<y.
intros x y z A.
apply (satz73a (satz44 A (satz38 _ _  (redAx2 _)) (satz38 _ _  (redAx2 _)))).
Qed.

Theorem satz106b {x y z:prat} : x*z=y*z -> x=y.
intros x y z A. apply eq_prat_equiv_f.
apply (satz73b (redAx1_rev _ _ (eq_prat_equiv_a A))).
Qed.

Theorem satz107 {x y z u:prat} : x<y -> z<u -> x*z<y*u.
intros x y z u A B.
apply (satz44 (satz74a A B) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz108a {x y z u:prat} : x<=y -> z<u -> x*z<y*u.
intros x y z u A B.
apply (satz44 (satz75a A B) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz108b {x y z u:prat} : x<y -> z<=u -> x*z<y*u.
intros x y z u A B.
apply (satz44 (satz75b A B) (redAx2 _) (redAx2 _)).
Qed.

Theorem satz109 {x y z u:prat} : x<=y -> z<=u -> x*z<=y*u.
intros x y z u A B.
generalize (satz76a A B); intros C. apply frac_order_equiv_d.
destruct (frac_order_equiv_c C) as [D|D].
left. apply eq_prat_equiv_c. unfold mul_prat. unfold eq_prat_a.
simpl. apply (redAx1 _ _ D). 
right. apply (satz44 D (redAx2 _) (redAx2 _)).
Qed.

Definition inv_mul_prat (x:prat) : prat := inv_mul_frac (rep x).

Theorem inv_mul_prat_correct_a : inverse_l prat O mul_prat inv_mul_prat.
intros [x xrp]. apply eq_prat_equiv_b.
unfold inv_mul_prat, mul_prat, rep,
frac_to_prat, eq_prat_a, nat_to_frac, rep.
apply redAx1.
apply (@satz39 _ (mul_frac (inv_mul_frac x) x)).
apply (satz68 (satz38 _ _ (redAx2 _)) (satz37 _)).
apply inv_mul_frac_correct.
Qed.

Lemma inv_mul_prat_correct_b (x:prat) : inv_mul_prat (inv_mul_prat x) = x.
intros x.
apply (@satz106b _ _ (inv_mul_prat x)).
rewrite inv_mul_prat_correct_a.
rewrite satz102.
symmetry.
apply inv_mul_prat_correct_a.
Qed.

Lemma inv_mul_prat_correct_c (x y:prat) : x < y -> inv_mul_prat y < inv_mul_prat x.
intros x y A.
apply (@satz106a _ _ y).
rewrite inv_mul_prat_correct_a,satz102.
apply (@satz106a _ _ x).
rewrite satz103,satz102,inv_mul_prat_correct_a.
apply (satz105a A).
Qed.

Theorem mul_prat_identity_l : identity_l prat O mul_prat.
intros [[x1 x2] xrp]. unfold mul_prat. simpl. rewrite (satz29 O), (satz29 O).
simpl. symmetry. unfold fred in xrp.
apply eq_prat_equiv_b. unfold eq_prat_a,frac_to_prat,rep.
apply (eq_frac_equiv_b xrp).
Qed.

(* quotient (x1/x2)/(y1/y2) = (x1*y2)/(x2*y1)*)
Definition quotient_prat (x y:prat):prat := x * inv_mul_prat y.

Lemma quotient_prat_correct_a (x y:prat) : (quotient_prat x y) * y = x.
intros x y; symmetry. unfold quotient_prat.
rewrite satz103, inv_mul_prat_correct_a.
symmetry. rewrite satz102. apply mul_prat_identity_l.
Qed.

Lemma quotient_prat_correct_b (x y:prat) : quotient_prat x y = mul_prat (quotient_prat O y) x.
intros x y.
apply (@satz106b _ _ y).
rewrite quotient_prat_correct_a.
rewrite satz103, (satz102 x y), <-satz103.
rewrite quotient_prat_correct_a.
symmetry. apply mul_prat_identity_l.
Qed. 

Theorem satz110a {x y:prat} : exists u, y*u = x.
intros x y.
destruct (@satz77a (rep x) (rep y)) as [z A].
exists z.
apply eq_prat_equiv_f. unfold eq_prat_b. unfold mul_prat. simpl.
apply (satz39 _ _ _  (satz39 _ _ _  (satz38 _ _  (redAx2 _)) 
              (satz68 (satz37 _) (satz38 _ _  (redAx2 _)))) A).
Qed.

Theorem satz110b {x y v w:prat} : v*y = x -> w*y=x -> v=w.
intros x y v w A B.
apply eq_prat_equiv_f. unfold eq_prat_b.
apply (@satz77b (rep x) (rep y)).
apply (satz39 _ _ _  (redAx2 _) (eq_prat_equiv_e A)).
apply (satz39 _ _ _  (redAx2 _) (eq_prat_equiv_e B)).
Qed.

(** We want to show that nat is a subset of prat. Hence we map every nat to a unique prat.
This prat should have the property of an integer *)

(** Landau's definition of int for prat *)
Definition prat_is_integer (x:prat) := exists u, u/O~rep x.

Lemma nat_to_prat_injective {x y:nat} : @eq prat x y -> x = y.
intros x y. intros A.
generalize (eq_prat_equiv_e A).
unfold nat_to_frac. unfold frac_to_prat. unfold eq_prat_b.
unfold rep.
apply red_equiv_a.
Qed.


(** We now have to show that nat_to_prat respects the operations and relations of nat and prat *)

Lemma nat_to_prat_resp_add {x y:nat} : x + y = add_nat x y.
intros x y. unfold add_prat.
unfold frac_to_prat. unfold rep. apply eq_prat_equiv_b.
unfold eq_prat_a. unfold rep. apply redAx1.
apply (satz39 _ _ _  (satz56 (satz38 _ _  (redAx2 _)) (satz38 _ _  (redAx2 _)))).
apply satz37.
Qed.

Lemma nat_to_prat_resp_mul {x y:nat} : x * y = mul_nat x y.
intros x y. unfold mul_prat. unfold frac_to_prat. unfold rep.
apply eq_prat_equiv_b; unfold eq_prat_a. unfold rep.
apply redAx1.
apply (satz39 _ _ _  (satz68 (satz38 _ _  (redAx2 _)) (satz38 _ _  (redAx2 _)))).
apply satz37.
Qed.

Lemma nat_to_prat_resp_leq {x y:nat} : x <= y <-> leq_nat x y.
intros x y. unfold frac_to_prat. unfold leq_prat. unfold rep.
unfold eq_frac_prop.
split. intros A.
generalize (frac_order_equiv_c A); intros [B|C].
apply nat_order_equiv_f. left. apply (red_equiv_a _ _ B).
apply nat_order_equiv_f. right.
apply (satz44 C (satz38 _ _  (redAx2 _)) (satz38 _ _  (redAx2 _))).
intros A. 
cut (x/O <~ y/O). intros B. apply (satz46 B (redAx2 _) (redAx2 _)).
apply frac_order_equiv_d.
destruct (nat_order_equiv_e A). rewrite H. left. apply satz37.
right. apply H.
Qed.

Lemma nat_to_prat_O : @eq prat O (O/O).
reflexivity.
Qed.

Lemma nat_to_prat_S {x:nat} : x + O = S x.
intros x. apply (@nat_to_prat_resp_add x O).
Qed.


Theorem satz112a {x y:nat} : add_frac (x/O) (y/O) ~ (add_nat x y)/O.
intros x y.
exact satz57.
Qed.

Theorem satz112b {x y:nat} : mul_frac (x/O) (y/O) ~ (mul_nat x y)/O.
intros x y.
reflexivity.
Qed.

Theorem satz114 {x y:nat} {z:prat} : frac_to_prat (x/y) = z -> mul_prat y z = x.
intros x y [[xr1 xr2] xrp] A.
apply (eq_prat_equiv_f).
unfold eq_prat_b,mul_prat,frac_to_prat,rep.
apply red_equiv_b.
generalize (eq_prat_equiv_e A); intros B.
unfold eq_prat_b,frac_to_prat,rep in B.
apply (satz39 _ _ _  (satz68 (satz38 _ _  (redAx2 _)) (satz39 _ _ _  (satz38 _ _  B) (satz38 _ _  (redAx2 _))))).
unfold nat_to_frac,mul_frac.
rewrite (satz29 y x). apply (satz38 _ _  (satz40)).
Qed.

Theorem satz115 {x y:prat} : exists z:nat, y < z*x.
intros [[x1 x2] xrp] [[y1 y2] yrp]. exists (add_nat (mul_nat y1 x2) O). unfold mul_prat.
unfold frac_to_prat. unfold lt_prat.
unfold nat_to_frac. unfold frac_to_prat. unfold rep.
cut (lt_frac (y1/y2)(mul_frac (red(S (mul_nat y1 x2)/O)) (x1/x2))).
intros A.
apply (satz44 A). apply satz37.
apply redAx2.
cut (lt_frac (y1/y2) (mul_frac (S (mul_nat y1 x2)/O) (x1/x2))).
intros A.
apply (satz44 A).
apply satz38. apply satz37.
apply (satz39 _ _ _  (satz68 (redAx2 _) (satz37 _))).
apply satz37.
unfold mul_frac.
rewrite (satz29 O x2).
unfold lt_frac.
rewrite satz31.
apply leq_nat_mul_const.
Qed.

Lemma prat_rep (x:prat) : exists x1 : nat, exists x2 : nat, quotient_prat x1 x2 = x.
intros [[x1 x2] xrp]. exists x1. exists x2.
apply (@satz106b _ _ x2).
rewrite quotient_prat_correct_a.
apply eq_prat_equiv_b.
unfold mul_prat, frac_to_prat, eq_prat_a, rep.
apply redAx1.
unfold nat_to_frac.
apply (satz39 _ (mul_frac (x1/x2) (x2/O))).
reflexivity.
apply (satz68 (satz37 _) (redAx2 _)).
Qed.

Theorem prat_minimal : PositiveRational_minimal prat O add_prat mul_prat inv_mul_prat.
intros set base A B C x.
destruct (prat_rep x) as [x1 [x2 D]].
rewrite <- D. apply B.
generalize x1; fix IHx3 1. intros [|x3]. apply base. rewrite <- nat_to_prat_S.
apply (A x3 O (IHx3 x3) base).
apply C.
generalize x2; fix IHx3 1. intros [|x3]. apply base. rewrite <- nat_to_prat_S.
apply (A x3 O (IHx3 x3) base).
Qed.


(* End of prats *)