Timings for Archimedean.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-unimath.dev//./UniMath/Algebra/Archimedean.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-unimath.dev//./UniMath/Algebra/Archimedean.v.timing
(** * Archimedean property *)
(** ** Preamble *)
(** Settings *)
Unset Kernel Term Sharing.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Algebra.RigsAndRings.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.Algebra.DivisionRig.
Require Import UniMath.Algebra.Domains_and_Fields.
Require Import UniMath.Algebra.ConstructiveStructures.
Require Import UniMath.MoreFoundations.Tactics.
Import UniMath.Algebra.Monoids.AddNotation.
(** ** The standard function from the natural numbers to a monoid *)
Fixpoint natmult {X : monoid} (n : nat) (x : X) : X :=
match n with
| O => 0%addmonoid
| S O => x
| S m => (x + natmult m x)%addmonoid
end.
Definition nattorig {X : rig} (n : nat) : X :=
natmult (X := rigaddabmonoid X) n 1%rig.
Definition nattoring {X : ring} (n : nat) : X :=
nattorig (X := ringtorig X) n.
Lemma natmultS :
∏ {X : monoid} (n : nat) (x : X),
natmult (S n) x = (x + natmult n x)%addmonoid.
Lemma nattorigS {X : rig} :
∏ (n : nat), nattorig (X := X) (S n) = (1 + nattorig n)%rig.
now apply (natmultS (X := rigaddabmonoid X)).
Lemma nattorig_natmult :
∏ {X : rig} (n : nat) (x : X),
(nattorig n * x)%rig = natmult (X := rigaddabmonoid X) n x.
rewrite nattorigS, natmultS.
now rewrite rigrdistr, IHn, riglunax2.
Lemma natmult_plus :
∏ {X : monoid} (n m : nat) (x : X),
natmult (n + m) x = (natmult n x + natmult m x)%addmonoid.
induction n as [|n IHn] ; intros m x.
change (S n + m)%nat with (S (n + m))%nat.
rewrite !natmultS, IHn, assocax.
Lemma nattorig_plus :
∏ {X : rig} (n m : nat),
(nattorig (n + m) : X) = (nattorig n + nattorig m)%rig.
apply (natmult_plus (X := rigaddabmonoid X)).
Lemma natmult_mult :
∏ {X : monoid} (n m : nat) (x : X),
natmult (n * m) x = (natmult n (natmult m x))%addmonoid.
induction n as [|n IHn] ; intros m x.
assert (H : S n = (n + 1)%nat).
rewrite <- plus_n_Sm, natplusr0.
rewrite !natmult_plus, IHn.
Lemma nattorig_mult :
∏ {X : rig} (n m : nat),
(nattorig (n * m) : X) = (nattorig n * nattorig m)%rig.
rewrite (natmult_mult (X := rigaddabmonoid X)), <- nattorig_natmult.
Lemma natmult_op {X : monoid} :
∏ (n : nat) (x y : X),
(x + y = y + x)%addmonoid
-> natmult n (x + y)%addmonoid = (natmult n x + natmult n y)%addmonoid.
rewrite natmultS, assocax, IHn, <- (assocax _ y).
assert (X1 : (y + natmult n x = natmult n x + y)%addmonoid).
rewrite !natmultS, <- assocax, <- X0, !assocax, IHn.
rewrite X1, assocax, <- natmultS, <- assocax, <- natmultS.
Lemma natmult_binophrel {X : monoid} (R : hrel X) :
istrans R -> isbinophrel R ->
∏ (n : nat) (x y : X), R x y -> R (natmult (S n) x) (natmult (S n) y).
rewrite !(natmultS (S _)).
Definition setquot_aux {X : monoid} (R : hrel X) : hrel X :=
λ x y : X, ∃ c : X, R (x + c)%addmonoid (y + c)%addmonoid.
Lemma istrans_setquot_aux {X : abmonoid} (R : hrel X) :
istrans R -> isbinophrel R -> istrans (setquot_aux R).
intros (c1,Hc1) (c2,Hc2).
exists (c1 + c2)%addmonoid.
rewrite assocax, (commax _ c1), <- !assocax.
Lemma isbinophrel_setquot_aux {X : abmonoid} (R : hrel X) :
isbinophrel R -> isbinophrel (setquot_aux R).
rewrite !assocax, (commax _ z), <- !assocax.
Lemma isequiv_setquot_aux {X : abmonoid} (R : hrel X) :
isinvbinophrel R ->
∏ x y : X, (setquot_aux R) x y <-> R x y.
(** ** Archimedean property in a monoid *)
Definition isarchmonoid {X : abmonoid} (R : hrel X) :=
∏ x y1 y2 : X,
R y1 y2 ->
(∃ n : nat, R (natmult n y1 + x)%addmonoid (natmult n y2))
× (∃ n : nat, R (natmult n y1) (natmult n y2 + x)%addmonoid).
Definition isarchmonoid_1 {X : abmonoid} (R : hrel X) :
isarchmonoid R ->
∏ x y1 y2 : X,
R y1 y2 ->
∃ n : nat, R (natmult n y1 + x)%addmonoid (natmult n y2) :=
λ H x y1 y2 Hy, (pr1 (H x y1 y2 Hy)).
Definition isarchmonoid_2 {X : abmonoid} (R : hrel X) :
isarchmonoid R ->
∏ x y1 y2 : X,
R y1 y2 ->
∃ n : nat, R (natmult n y1) (natmult n y2 + x)%addmonoid :=
λ H x y1 y2 Hy, (pr2 (H x y1 y2 Hy)).
(** ** Archimedean property in a group *)
Definition isarchgr {X : abgr} (R : hrel X) :=
∏ x y1 y2 : X,
R y1 y2 ->
∃ n : nat, R (natmult n y1 + x)%addmonoid (natmult n y2).
Local Lemma isarchgr_isarchmonoid_aux {X : abgr} (R : hrel X) :
isbinophrel R ->
∏ (n : nat) (x y1 y2 : X),
R (natmult n y1 * grinv X x)%multmonoid (natmult n y2) -> R (natmult n y1) (natmult n y2 * x)%multmonoid.
apply (pr2 (isinvbinophrelgr _ Hop) _ _ (grinv X x)).
rewrite assocax, (grrinvax X), runax.
Lemma isarchgr_isarchmonoid {X : abgr} (R : hrel X) :
isbinophrel R ->
isarchgr R ->
isarchmonoid (X := abgrtoabmonoid X) R.
generalize (H (grinv X x) _ _ Hy).
apply isarchgr_isarchmonoid_aux.
Lemma isarchmonoid_isarchgr {X : abgr} (R : hrel X) :
isarchmonoid (X := abgrtoabmonoid X) R ->
isarchgr R.
apply (isarchmonoid_1 _ H x y1 y2 Hy).
Local Lemma isarchabgrdiff_aux {X : abmonoid} (R : hrel X)
(Hr : isbinophrel R)
(Hr' : istrans R)
(y1 y2 x : abmonoiddirprod X X)
(n1 : nat)
(Hn1 : setquot_aux R (natmult n1 (pr1 y1 * pr2 y2) * pr1 x)%multmonoid
(natmult n1 (pr1 y2 * pr2 y1)%multmonoid))
(n2 : nat)
(Hn2 : setquot_aux R (natmult n2 (pr1 y1 * pr2 y2)%multmonoid)
(natmult n2 (pr1 y2 * pr2 y1) * pr2 x)%multmonoid) :
abgrdiffrel X Hr
(natmult (X := abgrdiff X) (n1 + n2) (setquotpr (binopeqrelabgrdiff X) y1) *
setquotpr (binopeqrelabgrdiff X) x)%multmonoid
(natmult (X := abgrdiff X) (n1 + n2) (setquotpr (binopeqrelabgrdiff X) y2)).
assert (H0 : ∏ n y, natmult (X := abgrdiff X) n (setquotpr (binopeqrelabgrdiff X) y) = setquotpr (binopeqrelabgrdiff X) (natmult n (pr1 y) ,, natmult n (pr2 y))).
intros (c1,Hc1) (c2,Hc2).
exists (c1 * c2)%multmonoid.
assert (X0 : (natmult (n1 + n2) (pr1 y1) * pr1 x * natmult (n1 + n2) (pr2 y2) * (c1 * c2) = (natmult n1 (pr1 y1 * pr2 y2) * pr1 x * c1) * (natmult n2 (pr1 y1 * pr2 y2) * c2))%multmonoid).
rewrite !natmult_op, !natmult_plus, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
assert (X0 : (natmult (n1 + n2) (pr1 y2) * (natmult (n1 + n2) (pr2 y1) * pr2 x) * (c1 * c2) = (natmult n1 (pr1 y2 * pr2 y1) * c1) * (natmult n2 (pr1 y2 * pr2 y1) * pr2 x * c2))%multmonoid).
rewrite !natmult_op, !natmult_plus, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
rewrite commax, !assocax.
Lemma isarchabgrdiff {X : abmonoid} (R : hrel X) (Hr : isbinophrel R) :
istrans R ->
isarchmonoid (setquot_aux R) ->
isarchgr (X := abgrdiff X) (abgrdiffrel X (L := R) Hr).
simple refine (setquotuniv3prop _ (λ x y1 y2, (abgrdiffrel X Hr y1 y2 ->
∃ n : nat, abgrdiffrel X Hr (natmult (X := abgrdiff X) n y1 * x)%multmonoid (natmult (X := abgrdiff X) n y2)) ,, _) _).
abstract apply isapropimpl, propproperty.
2: apply (isarchmonoid_1 _ H (pr1 x) (pr1 y1 * pr2 y2)%multmonoid (pr1 y2 * pr2 y1)%multmonoid), Hy.
2: apply (isarchmonoid_2 _ H (pr2 x) (pr1 y1 * pr2 y2)%multmonoid (pr1 y2 * pr2 y1)%multmonoid), Hy.
exists (pr1 n1 + pr1 n2)%nat.
apply isarchabgrdiff_aux.
(** ** Archimedean property in a rig *)
Definition isarchrig {X : rig} (R : hrel X) :=
(∏ y1 y2 : X, R y1 y2 -> ∃ n : nat, R (nattorig n * y1)%rig (1 + nattorig n * y2)%rig)
× (∏ x : X, ∃ n : nat, R (nattorig n) x)
× (∏ x : X, ∃ n : nat, R (nattorig n + x)%rig 0%rig).
Definition isarchrig_diff {X : rig} (R : hrel X) :
isarchrig R ->
∏ y1 y2 : X, R y1 y2 -> ∃ n : nat, R (nattorig n * y1)%rig (1 + nattorig n * y2)%rig :=
pr1.
Definition isarchrig_gt {X : rig} (R : hrel X) :
isarchrig R ->
∏ x : X, ∃ n : nat, R (nattorig n) x :=
λ H, (pr1 (pr2 H)).
Definition isarchrig_pos {X : rig} (R : hrel X) :
isarchrig R ->
∏ x : X, ∃ n : nat, R (nattorig n + x)%rig 0%rig :=
λ H, (pr2 (pr2 H)).
Lemma isarchrig_setquot_aux {X : rig} (R : hrel X) :
isinvbinophrel (X := rigaddabmonoid X) R
→ isarchrig R
→ isarchrig (setquot_aux (X := rigaddabmonoid X) R).
generalize (isarchrig_diff R H y1 y2 (pr2 Hr _ _ _ (pr2 Hy))).
generalize (isarchrig_gt R H x).
generalize (isarchrig_pos R H x).
Local Lemma isarchrig_isarchmonoid_1_aux {X : rig} (R : hrel X)
(Hr1 : R 1%rig 0%rig)
(Hr : istrans R)
(Hop1 : isbinophrel (X := rigaddabmonoid X) R)
(x y1 y2 : rigaddabmonoid X)
(m : nat)
(Hm : R (nattorig m * y1)%ring (1%rig + nattorig m * y2)%ring)
(n : nat)
(Hn : R (nattorig n + x)%ring 0%rig) :
R (natmult (max 1 n * m) y1 * x)%multmonoid
(natmult (max 1 n * m) y2).
rewrite !nattorig_natmult in Hm.
rewrite <- (lunax _ (natmult m y2)).
rewrite <- (runax _ (natmult (S n * m) y2)).
change BinaryOperations.op1 with (BinaryOperations.op (X := rigaddabmonoid X)).
rewrite natmult_op, assocax, <- natmult_mult.
Local Lemma isarchrig_isarchmonoid_2_aux {X : rig} (R : hrel X)
(Hr1 : R 1%rig 0%rig)
(Hr : istrans R)
(Hop1 : isbinophrel (X := rigaddabmonoid X) R)
(x y1 y2 : rigaddabmonoid X)
(m : nat)
(Hm : R (nattorig m * y1)%ring (1%rig + nattorig m * y2)%ring)
(n : nat)
(Hn : R (nattorig n) x) :
R (natmult (max 1 n * m) y1)
(natmult (max 1 n * m) y2 * x)%multmonoid.
rewrite !nattorig_natmult in Hm.
change BinaryOperations.op1 with (BinaryOperations.op (X := rigaddabmonoid X)).
rewrite natmult_op, <- natmult_mult.
Lemma isarchrig_isarchmonoid {X : rig} (R : hrel X) :
R 1%rig 0%rig ->
istrans R -> isbinophrel (X := rigaddabmonoid X) R ->
isarchrig R -> isarchmonoid (X := rigaddabmonoid X) R.
intros Hr1 Hr Hop1 H x y1 y2 Hy.
generalize (isarchrig_diff _ H _ _ Hy) (isarchrig_pos _ H x).
exists (max 1 (pr1 n) * (pr1 m))%nat.
apply isarchrig_isarchmonoid_1_aux.
generalize (isarchrig_diff _ H _ _ Hy) (isarchrig_gt _ H x).
exists (max 1 (pr1 n) * (pr1 m))%nat.
apply isarchrig_isarchmonoid_2_aux.
Lemma isarchmonoid_isarchrig {X : rig} (R : hrel X) :
(R 1%rig 0%rig)
-> isarchmonoid (X := rigaddabmonoid X) R
-> isarchrig R.
generalize (isarchmonoid_2 _ H 1%rig y1 y2 Hy).
abstract (rewrite !nattorig_natmult, rigcomm1 ;
exact (pr2 n)).
generalize (isarchmonoid_2 _ H x _ _ H01).
abstract (
pattern x at 1;
rewrite <- (riglunax1 X x) ;
pattern (0%rig : X) at 1;
rewrite <- (rigmultx0 X (nattorig (pr1 n))) ;
rewrite nattorig_natmult ;
exact (pr2 n)).
generalize (isarchmonoid_1 _ H x _ _ H01).
abstract (
pattern (0%rig : X) at 1;
rewrite <- (rigmultx0 X (nattorig (pr1 n))), nattorig_natmult ;
exact (pr2 n)).
(** ** Archimedean property in a ring *)
Definition isarchring {X : ring} (R : hrel X) :=
(∏ x : X, R x 0%ring -> ∃ n : nat, R (nattoring n * x)%ring 1%ring)
× (∏ x : X, ∃ n : nat, R (nattoring n) x).
Definition isarchring_1 {X : ring} (R : hrel X) :
isarchring R ->
∏ x : X, R x 0%ring -> ∃ n : nat, R (nattoring n * x)%ring 1%ring := pr1.
Definition isarchring_2 {X : ring} (R : hrel X) :
isarchring R ->
∏ x : X, ∃ n : nat, R (nattoring n) x := pr2.
Lemma isarchring_isarchrig {X : ring} (R : hrel X) :
isbinophrel (X := rigaddabmonoid X) R ->
isarchring R -> isarchrig (X := ringtorig X) R.
assert (X0 : R (y1 - y2)%ring 0%ring).
abstract (apply (pr2 (isinvbinophrelgr X Hop1)) with y2 ;
change BinaryOperations.op with (@BinaryOperations.op1 X) ;
rewrite ringassoc1, ringlinvax1, ringlunax1, ringrunax1 ;
exact Hy).
generalize (isarchring_1 _ H _ X0).
abstract
(rewrite <- (ringrunax1 _ (nattorig (pr1 n) * y1)%ring), <- (ringlinvax1 _ (nattorig (pr1 n) * y2)%ring), <- ringassoc1 ;
apply (pr2 Hop1) ;
rewrite <- ringrmultminus, <- ringldistr ;
exact (pr2 n)).
generalize (isarchring_2 _ H (- x)%ring).
abstract (change 0%rig with (0%ring : X) ;
rewrite <- (ringlinvax1 _ x) ;
apply (pr2 Hop1) ;
exact (pr2 n)).
Lemma isarchrig_isarchring {X : ring} (R : hrel X) :
isbinophrel (X := rigaddabmonoid X) R ->
isarchrig (X := ringtorig X) R -> isarchring R.
generalize (isarchrig_diff _ H _ _ Hx).
rewrite <- (ringrunax1 _ 1%ring), <- (ringmultx0 _ (nattoring n)).
apply (isarchrig_gt (X := ringtorig X)).
Lemma isarchring_isarchgr {X : ring} (R : hrel X) :
R 1%ring 0%ring ->
istrans R ->
isbinophrel (X := X) R ->
isarchring R -> isarchgr (X := X) R.
apply isarchmonoid_isarchgr.
apply (isarchrig_isarchmonoid (X := X)).
now apply isarchring_isarchrig.
Lemma isarchgr_isarchring {X : ring} (R : hrel X) :
R 1%ring 0%ring ->
istrans R ->
isbinophrel (X := X) R ->
isarchgr (X := X) R -> isarchring R.
apply isarchrig_isarchring.
apply isarchmonoid_isarchrig.
now apply (isarchgr_isarchmonoid (X := X)).
Theorem isarchrigtoring :
∏ (X : rig) (R : hrel X) (Hr : R 1%rig 0%rig)
(Hadd : isbinophrel (X := rigaddabmonoid X) R)
(Htra : istrans R)
(Harch : isarchrig (setquot_aux (X := rigaddabmonoid X) R)), isarchring (X := rigtoring X) (rigtoringrel X Hadd).
apply isarchgr_isarchring.
abstract (apply hinhpr ; simpl ;
exists 0%rig ; rewrite !rigrunax1 ;
exact Hr).
now apply (istransabgrdiffrel (rigaddabmonoid X)).
now generalize Hadd ; apply isbinopabgrdiffrel.
apply (isarchabgrdiff (X := rigaddabmonoid X)).
apply isarchrig_isarchmonoid.
abstract (apply hinhpr ; simpl ;
exists 0%rig ; rewrite !rigrunax1 ;
exact Hr).
(now apply (istrans_setquot_aux (X := rigaddabmonoid X))).
(now apply (isbinophrel_setquot_aux (X := rigaddabmonoid X))).
(* Proof without (Hr : R 1%rig 0%rig)
split.
- intros xx Hx0.
generalize (pr1 (pr2 xx)).
apply hinhuniv ; intros (x,Hx).
rewrite <- (setquotl0 _ xx (x,,Hx)) in Hx0 |- * ; simpl pr1 in Hx0 |- * ; clear xx Hx.
eapply hinhfun.
2: apply (isarchrig_diff _ Harch (pr1 x) (pr2 x)).
intros (n,Hn).
exists n.
assert ((nattoring (X := rigtoring X) n * setquotpr
(binopeqrelabgrdiff (rigaddabmonoid X)) x)%ring = (setquotpr
(binopeqrelabgrdiff (rigaddabmonoid X)) (nattorig n * pr1 x ,,
nattorig n * pr2 x))%ring).
{ clear.
induction n as [|n IHn].
- rewrite !rigmult0x, ringmult0x.
reflexivity.
- unfold nattoring.
rewrite !nattorigS, !rigrdistr, ringrdistr, !riglunax2, ringlunax2.
simpl.
eapply pathscomp0.
apply maponpaths.
apply IHn.
reflexivity. }
rewrite X0 ; clear X0.
revert Hn.
apply hinhfun ; simpl.
intros (c,Hc).
exists c.
rewrite rigrunax1.
exact Hc.
revert Hx0.
apply hinhfun ; simpl.
intros (c,Hc).
exists c.
rewrite riglunax1, rigrunax1 in Hc.
exact Hc.
- intros xx.
generalize (pr1 (pr2 xx)).
apply hinhuniv ; intros (x,Hx).
rewrite <- (setquotl0 _ xx (x,,Hx)) ; simpl pr1 ; clear xx Hx.
generalize (isarchrig_gt _ Harch (pr1 x)) (isarchrig_pos _ Harch (pr2 x)).
apply hinhfun2.
intros (n1,Hn1) (n2,Hn2).
exists (n1 + n2)%nat.
revert Hn1 Hn2.
assert (nattoring (X := rigtoring X) (n1 + n2) = setquotpr
(binopeqrelabgrdiff (rigaddabmonoid X)) (nattorig (n1 + n2) ,,
0%rig)).
{ generalize (n1 + n2) ; clear.
induction n as [|n IHn].
- reflexivity.
- unfold nattoring ; rewrite !nattorigS.
rewrite <- (riglunax1 _ 0%rig).
eapply pathscomp0.
apply maponpaths.
exact IHn.
reflexivity. }
rewrite X0 ; clear X0.
apply hinhfun2 ; simpl.
intros (c1,Hc1) (c2,Hc2).
exists (c1+c2)%rig.
eapply Htra.
assert (nattorig (n1 + n2) + pr2 x + (c1 + c2) =
((nattorig n1 + c1) + (nattorig n2 + pr2 x + c2)))%rig.
{ rewrite nattorig_plus, !rigassoc1.
apply maponpaths.
rewrite rigcomm1, !rigassoc1.
rewrite rigcomm1, !rigassoc1.
apply maponpaths.
rewrite rigcomm1, !rigassoc1.
reflexivity. }
simpl in X0 |- * ; rewrite X0 ; clear X0.
apply (pr2 Hadd).
exact Hc1.
rewrite rigrunax1, <- rigassoc1.
apply (pr1 Hadd).
rewrite riglunax1 in Hc2.
exact Hc2.*)
Lemma natmult_commringfrac {X : commring} {S : subabmonoid _} :
∏ n (x : X × S), natmult (X := commringfrac X S) n (setquotpr (eqrelcommringfrac X S) x) = setquotpr (eqrelcommringfrac X S) (natmult (X := X) n (pr1 x) ,, (pr2 x)).
apply (iscompsetquotpr (eqrelcommringfrac X S)).
apply (iscompsetquotpr (eqrelcommringfrac X S)).
rewrite <- (ringldistr X).
rewrite (ringcomm2 X (pr1 (pr2 x))).
Lemma isarchcommringfrac {X : commring} {S : subabmonoid _} (R : hrel X) Hop1 Hop2 Hs:
R 1%ring 0%ring ->
istrans R ->
isarchring R -> isarchring (X := commringfrac X S) (commringfracgt X S (R := R) Hop1 Hop2 Hs).
simple refine (setquotunivprop _ (λ _, (_,,_)) _).
apply isapropimpl, propproperty.
revert Hx ; apply hinhuniv ; intros (c,Hx) ; simpl in Hx.
rewrite !(ringmult0x X), (ringrunax2 X) in Hx.
apply (hinhfun (X := ∑ n, commringfracgt X S Hop1 Hop2 Hs (setquotpr (eqrelcommringfrac X S) ((nattoring n * pr1 x)%ring,, pr2 x)) 1%ring)).
rewrite (nattorig_natmult (X := commringfrac X S)).
rewrite (natmult_commringfrac (X := X) (S := S)).
rewrite <- (nattorig_natmult (X := X)).
generalize (isarchring_1 _ Hr _ Hx) (isarchring_2 _ Hr (pr1 (pr2 x) * pr1 c)%ring).
exists (max 1 n * m)%nat.
rewrite (ringrunax2 X), (ringlunax2 X), (ringassoc2 X).
rewrite (nattorig_natmult (X := X)), natmult_mult.
change (R
(natmult (succ n) (natmult (X := X) m (pr1 x)) * 1 * pr1 c)%ring
(1 * pr1 (pr2 x) * pr1 c)%ring).
rewrite <- (nattorig_natmult (X := X)), (ringrunax2 X), (ringlunax2 X), (ringassoc2 X), (nattorig_natmult (X := X)).
apply (natmult_binophrel (X := X) R).
rewrite <- (nattorig_natmult (X := X)), (ringassoc2 X).
simple refine (setquotunivprop _ _ _).
apply (hinhfun (X := ∑ n : nat, commringfracgt X S Hop1 Hop2 Hs
(setquotpr (eqrelcommringfrac X S) (nattoring n,, unel S))
(setquotpr (eqrelcommringfrac X S) x))).
unfold nattoring, nattorig.
change 1%rig with (setquotpr (eqrelcommringfrac X S)
(1%ring,, unel S)).
rewrite (natmult_commringfrac (X := X) (S := S) n).
generalize (isarchring_1 _ Hr _ (Hs (pr1 (pr2 x)) (pr2 (pr2 x)))) (isarchring_2 _ Hr (pr1 x)%ring).
exists (max 1 n * m)%nat.
apply (isringmultgttoisrringmultgt X).
change (n * m + m)%nat with (succ n * m)%nat.
apply (isringmultgttoisrringmultgt X).
rewrite (ringrunax2 X), (nattorig_natmult (X := X)), natmult_mult.
apply (natmult_binophrel (X := X) R).
rewrite <- (nattorig_natmult (X := X)).
(** ** Archimedean property in a field *)
Definition isarchfld {X : fld} (R : hrel X) :=
∏ x : X, ∃ n : nat, R (nattoring n) x.
Lemma isarchfld_isarchring {X : fld} (R : hrel X) :
∏ (Hadd : isbinophrel (X := rigaddabmonoid X) R) ( Hmult : isringmultgt X R)
(Hirr : isirrefl R),
isarchfld R -> isarchring R.
intros Hadd Hmult Hirr H.
case (fldchoice x) ; intros x'.
abstract (pattern (1%ring : X) at 1 ;
rewrite <- (pr1 (pr2 x')) ;
apply (isringmultgttoisrringmultgt _ Hadd Hmult _ _ _ Hx (pr2 n))).
abstract (apply fromempty ;
refine (Hirr _ _) ;
rewrite x' in Hx ;
apply Hx).
Lemma isarchring_isarchfld {X : fld} (R : hrel X) :
isarchring R -> isarchfld R.
apply (isarchring_2 R H x).
Theorem isarchfldfrac ( X : intdom ) ( is : isdeceq X ) { R : hrel X } ( is0 : @isbinophrel X R ) ( is1 : isringmultgt X R ) ( is2 : R 1%ring 0%ring ) ( nc : neqchoice R ) ( irr : isirrefl R ) ( tra : istrans R ) :
isarchring R -> isarchfld (X := fldfrac X is ) (fldfracgt _ is is0 is1 is2 nc).
apply isarchring_isarchfld.
generalize (isarchcommringfrac (X := X) (S := ringpossubmonoid X is1 is2) R is0 is1 (λ (c : X) (r : (ringpossubmonoid X is1 is2) c), r) is2 tra X0).
assert (H_f : ∏ n x, (weqfldfracgt_f X is is0 is1 is2 nc (nattoring n * x)%ring) = (nattoring n * weqfldfracgt_f X is is0 is1 is2 nc x)%ring).
rewrite (nattorig_natmult (X := fldfrac X is)), (nattorig_natmult (X := commringfrac X (@ringpossubmonoid X R is1 is2))).
refine (pr2 (pr1 (isringfunweqfldfracgt_f _ _ _ _ _ _ _))).
rewrite !natmultS, <- IHn.
refine (pr1 (pr1 (isringfunweqfldfracgt_f _ _ _ _ _ _ _)) _ _).
assert (H_0 : (weqfldfracgt_f X is is0 is1 is2 nc 0%ring) = 0%ring).
refine (pr2 (pr1 (isringfunweqfldfracgt_f _ _ _ _ _ _ _))).
assert (H_1 : (weqfldfracgt_f X is is0 is1 is2 nc 1%ring) = 1%ring).
refine (pr2 (pr2 (isringfunweqfldfracgt_f _ _ _ _ _ _ _))).
2: apply (isarchring_1 _ X1 (weqfldfracgt_f X is is0 is1 is2 nc x)).
2: apply (isarchring_2 _ X1 (weqfldfracgt_f X is is0 is1 is2 nc x)).
rewrite <- (ringrunax2 _ (nattoring n)), H_f, H_1, ringrunax2.
(** ** Archimedean property in a constructive field *)
Definition isarchCF {X : ConstructiveField} (R : hrel X) :=
∏ x : X, ∃ n : nat, R (nattoring n) x.
Lemma isarchCF_isarchring {X : ConstructiveField} (R : hrel X) :
∏ (Hadd : isbinophrel (X := rigaddabmonoid X) R) ( Hmult : isringmultgt X R)
(Hirr : isirrefl R),
(∏ x : X, R x 0%CF -> (x ≠ 0)%CF) ->
isarchCF R -> isarchring R.
intros Hadd Hmult Hirr H0 H.
generalize (H (CFinv x (H0 _ Hx))).
change 1%ring with (1%CF : X).
rewrite <- (islinv_CFinv x (H0 x Hx)).
apply isringmultgttoisrringmultgt.
Lemma isarchring_isarchCF {X : ConstructiveField} (R : hrel X) :
isarchring R -> isarchCF R.
apply (isarchring_2 R H x).