Library Zmod

Require Import ZArith.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Arith.Euclid.


Require Import Zfacts.
Require Import EnsembleFacts.

Open Local Scope Z_scope.

Section Zmod.

Definition Zmodequiv (a b N:Z) :Prop := exists k, a-b=k*N.

Parameter ZmodN : Z->Type.
Parameter Zmod : forall (N a:Z), ZmodN N.



Axiom Zmodequivalence_right: forall a b N:Z,
Zmodequiv a b N -> Zmod N a=Zmod N b.
Axiom Zmodequivalence_left: forall a b N:Z,
Zmod N a=Zmod N b -> Zmodequiv a b N.

Axiom Zmod_elim : forall (N:Z) (a:ZmodN N),
exists b:Z, Zmod N b=a.

Theorem Zmod_addition : forall (N a b c:Z),
 (Zmod N a)=(Zmod N b)->(Zmod N (a +c))=(Zmod N (b+c)).

Theorem Zmod_opp : forall (N a b:Z),
 (Zmod N a)=(Zmod N b)->(Zmod N (-a))=(Zmod N (-b)).

Parameter Zmod_add :
forall N:Z,(ZmodN N)->(ZmodN N)->(ZmodN N).

Axiom Zmod_add_Z: forall (N aZ bZ:Z) (a b:ZmodN N),
a=Zmod N aZ -> b=Zmod N bZ ->
 Zmod_add N a b=Zmod N (aZ+bZ).

Definition Zmod_repset (N:Z) (R:Ensemble Z):Prop:=
(forall a:ZmodN N,exists r:Z, Zmod N r=a /\ In Z R r)
/\
(forall r s:Z, In Z R r-> In Z R s-> s<>r
 -> Zmod N r<>Zmod N s).

Definition Zmod_repsetnat (N:Z) (R:Ensemble nat):Prop:=
(forall a:ZmodN N,exists r:nat, Zmod N (Z_of_nat r)=a
  /\ In nat R r)
/\
(forall r s:nat, In nat R r-> In nat R s-> s<>r
 -> Zmod N (Z_of_nat r)<>Zmod N (Z_of_nat s)).

Lemma Zmod_haspos : forall (N:Z) (a:ZmodN N), N>0->
exists n:Z, n>=0 /\ Zmod N n=a.

Theorem Zmod_canonical : forall (N:Z) (a:ZmodN N), N>0->
exists n:Z, 0<=n<N /\ Zmod N n=a.

Theorem Zmod_nat_repsetnat : forall (N:Z), N>0->
Zmod_repsetnat N (nat_firsts (Zabs_nat N)).

Theorem Zmod_addisbijection : forall (N:Z) (a:ZmodN N),
Bijective (ZmodN N) (ZmodN N) (fun x:ZmodN N=>Zmod_add N x a).




Theorem Zmodeg_equiv7_1_8 : Zmod 7 1=Zmod 7 8.

Theorem Zmodeg_add10_1_8 :
Zmod_add 10 (Zmod 10 1) (Zmod 10 8)=Zmod 10 9.

Print Zind.
Theorem Zmodeg_parity : forall a:ZmodN 2,
a=Zmod 2 0 \/ a=Zmod 2 1.
Print Zmod_elim.



Qed.

End Zmod.