Library Zfacts

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

Section Zfacts.

Open Local Scope Z_scope.

Inductive nat_firsts (N:nat) : Ensemble nat:=
|nat_firsts_def : forall n:nat, lt n N
->In nat (nat_firsts N) n.

Lemma Z_ge_mulpos : forall a b p:Z, p>=0 ->
 (a>=b -> a*p>=b*p).

Lemma Z_gt_mulpos : forall a b p:Z, p>0 ->
 (a>b -> a*p>b*p).

Lemma Z_getpositive : forall a:Z, a>0 ->
 exists p:positive, a=Zpos p.

Lemma Z_gt_divpos : forall a b p:Z, p>0 ->
 a*p>b*p -> a>b.

Lemma Z_ge_multwopos : forall a b:Z,
a>=0-> b>=0 -> a*b>=0.

Lemma Z_absnat_0 : Zabs_nat 0=0%nat.

Lemma Z_absnat_posge0 : forall (N:Z), N>=0 ->
ge (Zabs_nat N) (0%nat).

Lemma Z_absnat_posgt0 : forall (N:Z), N>0 ->
gt (Zabs_nat N) (0%nat).

Lemma Z_eucdiff : forall (N a b:Z),
0<=a<N -> 0<=b<N -> -N<a-b<N.

End Zfacts.