# Library Coq.micromega.ZCoeff

Require Import OrderedRing.
Require Import RingMicromega.
Require Import ZArith.
Require Import InitialRing.
Require Import Setoid.
Import OrderedRingSyntax.
Section InitialMorphism.
Variable R : Type.
Variables rO rI : R.
Variables rplus rtimes rminus: R -> R -> R.
Variable ropp : R -> R.
Variables req rle rlt : R -> R -> Prop.
Variable sor : SOR rO rI rplus rtimes rminus ropp req rle rlt.
Notation "0" := rO.
Notation "1" := rI.
Notation "x + y" := (rplus x y).
Notation "x * y " := (rtimes x y).
Notation "x - y " := (rminus x y).
Notation "- x" := (ropp x).
Notation "x == y" := (req x y).
Notation "x ~= y" := (~ req x y).
Notation "x <= y" := (rle x y).
Notation "x < y" := (rlt x y).
Lemma req_refl : forall x, req x x.
Lemma req_sym : forall x y, req x y -> req y x.
Lemma req_trans : forall x y z, req x y -> req y z -> req x z.
Add Relation R req
reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
as sor_setoid.
Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
Add Morphism ropp with signature req ==> req as ropp_morph.
Add Morphism rle with signature req ==> req ==> iff as rle_morph.
Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp.
Notation phi_pos := (gen_phiPOS 1 rplus rtimes).
Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes).
Notation "[ x ]" := (gen_order_phi_Z x).
Lemma ring_ops_wd : ring_eq_ext rplus rtimes ropp req.
Lemma Zring_morph :
ring_morph 0 1 rplus rtimes rminus ropp req
0%Z 1%Z Zplus Zmult Zminus Zopp
Zeq_bool gen_order_phi_Z.
Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x.
Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Psucc x) == 1 + phi_pos1 x.
Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
Lemma clt_morph : forall x y : Z, (x < y)%Z -> [ x ] < [ y ].
Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [ x ] <= [ y ].
Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [ x ] ~= [ y ].
End InitialMorphism.