Require Import structures.

Require Import naturals.

Definition nat_struct : NatStruct.
apply (mk_NatStruct nat O add_nat mul_nat (fun x y => x < y)).
intros x y. apply satz6.
intros x y z. apply satz5.
intros x y. apply satz29.
intros x y z. apply satz31.
exact mul_nat_identity_l.
intros x y z. apply satz30.
intros x. apply lt_nat_irreflexive.
exact satz15a.
exact satz10H0.
intros x y z. apply satz19a.
intros x y z. apply satz32a.
intros x y z. apply satz20b.
intros x y. apply satz7.
exact @axiom5.
Defined.

Require Import prats.

Definition prat_struct : PositiveRationalStruct.
apply (mk_PositiveRationalStruct prat O add_prat mul_prat inv_mul_prat lt_prat).
apply satz92.
apply satz93.
apply satz102.
apply satz103.
apply mul_prat_identity_l.
apply inv_mul_prat_correct_a.
apply satz104.
apply satz81H0.
apply satz86.
apply lt_prat_irreflexive.
exact @satz95.
exact @satz105a.
exact @satz91.
exact @satz90.
exact @satz89.
apply prat_minimal.
Defined.

Require Import reals.
Require Import completeness.

Definition real_struct_jh : RealStructJH.
apply (mk_RealStructJH real Z O add_real mul_real inv_add_real inv_mul_real' lt_real).
discriminate.
apply satz175.
apply satz186.
intros x. tauto.
intros x. apply satz179.
apply satz194.
apply satz199.
apply satz195.
intros x A.
assert (B:neq_zero x).
destruct x; simpl; tauto.
rewrite <-(inv_mul_real_equiv x B).
rewrite <-(satz204a O x B).
rewrite satz194.
apply (f_equal (fun z => x * z)).
unfold quotient_real.
rewrite satz195. tauto.
apply satz201.
apply satz167H0.
apply satz171.
intros x A.
apply (satz167H1 x x); tauto.
intros x y z A.
rewrite (satz175 x),(satz175 x).
apply (satz188a A).
intros x y A B.
generalize (satz203a _ _ y A (satz171 Z O _ I B));
intros C.
rewrite satz195 in C.
apply (satz171 _ _ _ B C).
apply HAsup.
Defined.

Definition real_struct_jd : RealStructJD.
apply (mk_RealStructJD real Z O add_real mul_real leq_real).
apply satz175.
apply satz186.
intros x. tauto.
intros x. exists (inv_add_real x).
apply satz179.
apply satz194.
apply satz199.
discriminate.
apply satz195.
intros x A.
assert (B:neq_zero x).
destruct x; simpl; tauto.
exists (inv_mul_real x B).
rewrite <-(satz204a O x B).
rewrite satz194.
apply (f_equal (fun z => x * z)).
unfold quotient_real.
rewrite satz195. tauto.
apply satz201.
apply satz173.
intros x y [A|A] [B|B].
destruct (satz167H2 _ _ A B).
destruct (satz167H1 _ _ A B).
destruct (satz167H1 _ _ B A).
apply A.
intros x y.
destruct (satz167H0 x y) as [H|[H|H]].
left. left. apply H.
left. right. apply H.
right. left. apply H.
intros x y z. repeat rewrite (satz175 x).
intros [A|A].
left. apply (satz188a A).
right. apply (satz188b A).
intros x y [A|A] [B|B].
left.
generalize (satz203a _ _ y A (satz171 Z O _ I B));
intros C.
rewrite satz195 in C.
apply (satz171 _ _ _ B C).
subst y.
left. rewrite satz194,satz195. apply A.
subst x. rewrite satz195. left. apply B.
subst x. rewrite satz195. right. apply B.
apply Arch.
intros a b A. apply NI.
intros n. destruct (A n); tauto.
intros n. destruct (A n); tauto.
intros n. destruct (A n); tauto.
Qed.

Definition real_struct_ta' : RealStructTA'.
apply (mk_RealStructTA' real O add_real lt_real).
exact satz167H0.
exact satz167H2.
exact tarski3.
exact tf.
exact tarski5.
exact tarski6.
exact tarski7.
exact tarski8.
Defined.

Definition real_struct_ta'' : RealStructTA''.
apply (mk_RealStructTA'' real Z O add_real mul_real lt_real).
apply satz167H0.
intros x y. apply satz167H2.
apply satz171.
apply tf.
apply satz175.
apply satz186.
intros x y.
exists (sub_real x y).
unfold sub_real.
rewrite (satz175 x),<-satz186,(satz175 y),satz179.
tauto.
intros x y z.
repeat rewrite (satz175 x).
apply satz188a.
intros x. rewrite satz175; tauto.
apply satz194.
apply satz199.
intros x y A.
assert (B:neq_zero y).
destruct y; simpl; tauto.
exists (quotient_real x y B).
symmetry. apply satz204a.
intros x y z A B.
repeat rewrite (satz194 x).
apply (satz203a _ _ _ B A).
apply satz201.
intros x; rewrite satz194; apply satz195.
intros A. discriminate A.
Defined.