NDiv.v

(****************************************************************************                                                                                         IEEE754  :  NDiv                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** Definition of the quotient and divisibility for natural and relative numbers*)
Require Import Omega.
Require Import Arith.
Require Import Compare.
Require Import Faux.
Require Import Euclid_proof.
Require Import Zpower.
Require Import Zcomplements.
Require Import Reals.
Require Import sTactic.
Require Import Digit.

(* We use the quotient function in Euclid proof to build our Nquotient *)

Definition Nquotient :=
   [m, n:nat]
      Cases n of
          O => O
         | (S n') =>
             Cases (quotient (S n') (lt_le_S O (S n') (lt_O_Sn n')) m) of
                 (exist x _) => x
             end
      end.
(* It has the required property *)

Theorem NquotientProp:
  (m, n:nat) (lt O n) ->
  (ex nat [r:nat]m=(plus (mult (Nquotient m n) n) r) /\ (lt r n)).

(* We lift this quotient to relative numbers *)

Definition ZNquotient :=
   [m:Z] [n:nat]
      Cases m of
          ZERO => ZERO
         | (POS x) => (INZ (Nquotient (absolu m) n))
         | (NEG x) => (Zopp (INZ (Nquotient (absolu m) n)))
      end.

Theorem ZNquotientProp:
  (m:Z) (n:nat) (lt O n) -> (absolu m)=(mult (Nquotient (absolu m) n) n) ->
  m=(Zmult (ZNquotient m n) (INZ n)).

(* The property of a  number to divide another one      (Ndivides n m) shoud be read as m divides n *)

Definition Ndivides := [n, m:nat](Ex [q:nat] n=(mult m q)).

Theorem NdividesNquotient:
  (n, m:nat) (lt O m) -> (Ndivides n m) ->n=(mult (Nquotient n m) m).

Theorem NdividesNquotientInv:
  (n, m:nat) n=(mult (Nquotient n m) m) ->(Ndivides n m).

Theorem NdividesMult:
  (n, m, p:nat) (Ndivides n m) ->(Ndivides (mult p n) (mult p m)).

Theorem NdividesDiv:
  (n, m, p:nat) (lt O p) -> (Ndivides (mult p n) (mult p m)) ->(Ndivides n m).

Definition dividesP: (n, m:nat){(Ndivides n m)}+{~ (Ndivides n m)}.

Theorem Nquotient1: (m:nat)(Nquotient m (1))=m.

Theorem ZNquotient1: (m:Z)(ZNquotient m (1))=m.

Theorem Ndivides1: (m:nat)(Ndivides m (1)).

Theorem NquotientUnique:
  (m, n, q, r:nat) (lt O n) -> m=(plus (mult q n) r) -> (lt r n) ->
  q=(Nquotient m n).

Theorem NquotientMonotone:
  (n, m, q:nat) ~ q=O -> (lt n m) ->(le (Nquotient n q) (Nquotient m q)).

Theorem ZNquotientMonotone:
  (n, m:Z) (q:nat) ~ q=O -> (Zlt n m) ->(Zle (ZNquotient n q) (ZNquotient m q)).

Theorem NotDividesDigit:
  (r:nat) (v:nat) (lt (1) r) -> ~ v=O ->~ (Ndivides v (exp r (digit r v))).

Theorem NDividesLt: (n, m:nat) ~ n=O -> (Ndivides n m) ->(le m n).

Theorem Nquotient_mult_comp:
  (m, n, p:nat) ~ n=O -> ~ p=O ->
  (Nquotient (mult m p) (mult n p))=(Nquotient m n).

Theorem ZNquotient_INZ:
  (m, n:nat) ~ n=O ->(ZNquotient (INZ m) n)=(inject_nat (Nquotient m n)).

Theorem ZNquotient_Zopp:
  (m:Z) (n:nat)(ZNquotient (Zopp m) n)=(Zopp (ZNquotient m n)).

Theorem ZNquotient_mult_comp:
  (m:Z) (n, p:nat) ~ n=O -> ~ p=O ->
  (ZNquotient (Zmult m (inject_nat p)) (mult n p))=(ZNquotient m n).

Theorem NDivides_add:
  (n, m, p:nat) (Ndivides n p) -> (Ndivides m p) ->(Ndivides (plus n m) p).

Theorem NDivides_minus:
  (n, m, p:nat) (Ndivides n p) -> (Ndivides m p) ->(Ndivides (minus n m) p).

Theorem NDivides_mult:
  (n, m, p, q:nat) (Ndivides n p) -> (Ndivides m q) ->
  (Ndivides (mult n m) (mult p q)).

Theorem NdividesTrans:
  (n, m, p:nat) (Ndivides n m) -> (Ndivides m p) ->(Ndivides n p).

Theorem NdividesLessExp:
  (n, m, p:nat) (le m p) ->(Ndivides (exp n p) (exp n m)).

30/05/01, 18:21