Require Import Basic.
Require Import RIneq.
Require Import Zq.
Require Import listT.
Require Import ZArith.
Require Import Rdefinitions.
Require Import Coq.Reals.Raxioms.
Require Import R_lemma.


(*---------------------------------------------------------------------------------------
this file provides somme lemmas, definitions and assumptions for the commutative field Zq
----------------------------------------------------------------------------------------*)

Variable q : nat.

Lemma lt_0_INRx : forall x : nat, (0 < Z_of_nat x)%Z -> (0 < INR x)%R.
intros.
induction  x as [| x Hrecx].
absurd (0 < 0)%Z.
auto with *.
exact H.
simpl in |- *.
case x.
auto with *.
intro; auto with *.
Qed.

Lemma Rlt_1_S : forall n : nat, (1 < INR (S n) + 1)%R.
simple induction n.
simpl in |- *.
auto with *.
intros.
replace (1 < INR (S (S n0)) + 1)%R with (1 + 0 < INR (S (S n0)) + 1)%R.
apply Rplus_lt_compat.
auto.
auto with *.
rewrite Rplus_0_r.
auto.
Qed.


Lemma lt_1_INRx : forall x : nat, (1 < Z_of_nat x)%Z -> (1 < INR x)%R.
intros.
induction  x as [| x Hrecx].
absurd (1 < 0)%Z.
auto with *.
apply H.
generalize H.
simpl in |- *.
case x.
simpl in |- *.
intro.
absurd (1 < 1)%Z.
auto with *.
auto with *.
intros.
apply Rlt_1_S.
Qed.

Section bornes_q.
Variable q : nat.
Hypothesis q_gt_1 : (1 < Z_of_nat q)%Z.
Lemma q_gt_0 : (0 < Z_of_nat q)%Z.
assert (1 < Z_of_nat q)%Z.
exact q_gt_1.
apply Zlt_trans with (m := 1%Z).
auto with zarith.
exact H.
Qed.

Lemma lt_1_INRq : (1 < INR q)%R.
apply lt_1_INRx.
exact q_gt_1.
Qed.

Lemma lt_0_INRq : (0 < INR q)%R.
apply lt_0_INRx.
exact q_gt_0.
Qed.
End bornes_q.



Hypotheses q_gt_1 : (1 < Z_of_nat q)%Z.



Definition Zqq := Zq q.
Definition eqZq : rel Zqq := mod_ (Z_of_nat q).

(* this function returns True if a belongs to l *)
Fixpoint memZq (a : Zqq) (l : listT Zqq) {struct l} : Prop :=
  match l with
  | nilT => False
  | consT x xs => eqZq a x \/ memZq a xs
  end.

(* this function returns True if there are some duplications in the list l *)
Definition doubles : listT Zqq -> Prop :=
  (fix doubles (l : listT Zqq) : Prop :=
     match l with
     | nilT => False
     | consT x xs => memZq x xs \/ doubles xs
     end).