(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "datatypes/sums.ma".
include "datatypes/list.ma".
include "Plogic/equality.ma".
include "binary/Z.ma".
include "binary/positive.ma".

nlemma eq_rect_Type0_r:
 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption.
nqed.

nlemma eq_rect_r2:
 ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
 #A; #a; #x; #p; ncases p; #P; #H; nassumption.
nqed.

nlemma eq_rect_Type2_r:
 ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
nqed.

nlemma eq_rect_CProp0_r:
 ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption.
nqed.

nlemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
#A;#x;#y;*;#H;napply nmk;#H';/2/;
nqed.

(* stolen from logic/connectives.ma to give Prop version. *)
notation > "hvbox(a break \liff b)"
  left associative with precedence 25
for @{ 'iff $a $b }.

notation "hvbox(a break \leftrightarrow b)"
  left associative with precedence 25
for @{ 'iff $a $b }.

interpretation "logical iff" 'iff x y = (iff x y).

(* bool *)

ndefinition xorb : bool → bool → bool ≝
  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
  

(* TODO: move to Z.ma *)

nlemma eqZb_z_z : ∀z.eqZb z z = true.
#z;ncases z;nnormalize;//;
nqed.

(* XXX: divides goes to arithmetics *)
ninductive dividesP (n,m:Pos) : Prop ≝
| witness : ∀p:Pos.m = times n p → dividesP n m.
interpretation "positive divides" 'divides n m = (dividesP n m).
interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).

ndefinition dividesZ : Z → Z → Prop ≝
λx,y. match x with
[ OZ ⇒ False
| pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
| neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ]
].

interpretation "integer divides" 'divides n m = (dividesZ n m).
interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).

(* should be proved in nat.ma, but it's not! *)
naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].

nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
#n m; napply eqb_elim; //; nqed.

nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
nnormalize;
#n;#m;ncases n;ncases m;nnormalize;//;
##[ ##1,2: #n';#H;ndestruct
##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); //
##] nqed.

nlemma reflexive_Zle : reflexive ? Zle.
#x; ncases x; //; nqed.

nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
#n;ncases n;nnormalize;//;nqed.

nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
#x; ncases x; //;
#n; ncases n; //; nqed.

nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
#x;#y;
napply pos_elim
 ##[ ##2: #n'; #IH; ##]
nrewrite > (Zplus_Zsucc_Zpred y ?);
##[ nrewrite > (Zpred_Zsucc (pos n'));
 #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??);
    napply Zsucc_le;
##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le;
##] nqed.

(* XXX: Zmax must go to arithmetics *)
ndefinition Zmax : Z → Z → Z ≝ 
  λx,y.match Z_compare x y with
  [ LT ⇒ y
  | _ ⇒ x ].

nlemma Zmax_l: ∀x,y. x ≤ Zmax x y.
#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
/3/; ncases x; /3/; nqed.

nlemma Zmax_r: ∀x,y. y ≤ Zmax x y.
#x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y);
ncases x; /3/; nqed.

ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
#x y; ncases x;
##[ ncases y;
  ##[ ##1,2: //
  ##| #n; napply False_ind;
  ##]
##| #n; ncases y;
  ##[ nnormalize; napply False_ind;
  ##| #m; napply (pos_cases … n); /2/;
  ##| #m; nnormalize; napply False_ind;
  ##]
##| #n; ncases y; /2/;
##] nqed.
    
ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
#n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt;
napply (transitive_Zle … Hle); /2/;
nqed.

ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
#z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H;
##[@;//
##|@2;//##]
nqed.

nlemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
#z1;#z2;nlapply (eqZb_to_Prop z1 z2); ncases (eqZb z1 z2); //;
#H; #H'; napply False_ind; napply (absurd ? H H');
nqed.

(* Z.ma *)

ndefinition Zge: Z → Z → Prop ≝
λn,m:Z.m ≤ n.

interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).

ndefinition Zgt: Z → Z → Prop ≝
λn,m:Z.m<n.

interpretation "integer 'greater than'" 'gt x y = (Zgt x y).

interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).

nlet rec Zleb (x:Z) (y:Z) : bool ≝
  match x with
  [ OZ ⇒ 
    match y with 
    [ OZ ⇒ true
    | pos m ⇒ true
    | neg m ⇒ false ]
  | pos n ⇒
    match y with 
    [ OZ ⇒ false
    | pos m ⇒ leb n m
    | neg m ⇒ false ]
  | neg n ⇒
    match y with 
    [ OZ ⇒ true
    | pos m ⇒ true
    | neg m ⇒ leb m n ]].
    
nlet rec Zltb (x:Z) (y:Z) : bool ≝
  match x with
  [ OZ ⇒
    match y with 
    [ OZ ⇒ false
    | pos m ⇒ true
    | neg m ⇒ false ]
  | pos n ⇒
    match y with 
    [ OZ ⇒ false
    | pos m ⇒ leb (succ n) m
    | neg m ⇒ false ]
  | neg n ⇒
    match y with 
    [ OZ ⇒ true
    | pos m ⇒ true
    | neg m ⇒ leb (succ m) n ]].



ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
#n;#m;ncases n;ncases m; //;
##[ ##1,2: #m'; nnormalize; #H; napply (False_ind ? H)
##| ##3,5: #n';#m'; nnormalize; napply le_to_leb_true;
##| ##4: #n';#m'; nnormalize; #H; napply (False_ind ? H)
##] nqed.

ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
#n;#m;ncases n;ncases m; //;
##[ ##1,2: #m'; nnormalize; #H; ndestruct
##| ##3,5: #n';#m'; nnormalize; napply leb_true_to_le;
##| ##4: #n';#m'; nnormalize; #H; ndestruct
##] nqed.

ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
#n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;
nqed.

ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
#n;#m;ncases n;ncases m; //;
##[ nnormalize; #H; napply (False_ind ? H)
##| ##2,3: #m'; nnormalize; #H; napply (False_ind ? H)
##| ##4,6: #n';#m'; nnormalize; napply le_to_leb_true;
##| #n';#m'; nnormalize; #H; napply (False_ind ? H)
##] nqed.

ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
#n;#m;ncases n;ncases m; //;
##[ nnormalize; #H; ndestruct
##| ##2,3: #m'; nnormalize; #H; ndestruct
##| ##4,6: #n';#m'; napply leb_true_to_le;
##| #n';#m'; nnormalize; #H; ndestruct
##] nqed.

ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
#n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;
nqed.

ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 
(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
#n;#m;#P;#Hle;#Hnle;
nlapply (refl ? (Zleb n m));
nelim (Zleb n m) in ⊢ ((???%)→%);
#Hb;
##[ napply Hle; napply (Zleb_true_to_Zle … Hb)
##| napply Hnle; napply (Zleb_false_to_not_Zle … Hb) 
##] nqed.

ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 
(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
#n;#m;#P;#Hlt;#Hnlt;
nlapply (refl ? (Zltb n m));
nelim (Zltb n m) in ⊢ ((???%)→%);
#Hb;
##[ napply Hlt; napply (Zltb_true_to_Zlt … Hb)
##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb) 
##] nqed.

nlet rec Z_times (x:Z) (y:Z) : Z ≝
match x with
[ OZ ⇒ OZ
| pos n ⇒
  match y with
  [ OZ ⇒ OZ
  | pos m ⇒ pos (n*m)
  | neg m ⇒ neg (n*m)
  ]
| neg n ⇒
  match y with
  [ OZ ⇒ OZ
  | pos m ⇒ neg (n*m)
  | neg m ⇒ pos (n*m)
  ]
].
interpretation "integer multiplication" 'times x y = (Z_times x y).

(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).

(* datatypes/list.ma *)

ntheorem nil_append_nil_both:
  ∀A:Type. ∀l1,l2:list A.
    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
#A l1 l2; ncases l1;
##[ ncases l2;
  ##[ /2/
  ##| #h t H; ndestruct;
  ##]
##| ncases l2;
  ##[ nnormalize; #h t H; ndestruct;
  ##| nnormalize; #h1 t1 h2 h3 H; ndestruct;
  ##]
##] nqed. 

(* division *)

ninductive natp : Type ≝
| pzero : natp
| ppos  : Pos → natp.

ndefinition natp0 ≝
λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].

ndefinition natp1 ≝
λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].

nlet rec divide (m,n:Pos) on m ≝ 
match m with 
[ one ⇒
  match n with
  [ one ⇒ 〈ppos one,pzero〉
  | _ ⇒ 〈pzero,ppos one〉
  ]
| p0 m' ⇒
  match divide m' n with
  [ mk_pair q r ⇒
    match r with
    [ pzero ⇒ 〈natp0 q,pzero〉
    | ppos r' ⇒
      match partial_minus (p0 r') n with
      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
      | MinusZero ⇒ 〈natp1 q, pzero〉
      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
      ]
    ]
  ]
| p1 m' ⇒
  match divide m' n with
  [ mk_pair q r ⇒
    match r with
    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
    | ppos r' ⇒
      match partial_minus (p1 r') n with
      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
      | MinusZero ⇒ 〈natp1 q, pzero〉
      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
      ]
    ]
  ]
].

ndefinition div ≝ λm,n. fst ?? (divide m n).
ndefinition mod ≝ λm,n. snd ?? (divide m n).

ndefinition pairdisc ≝ 
λA,B.λx,y:pair A B.
match x with 
[(mk_pair t0 t1) ⇒ 
match y with 
[(mk_pair u0 u1) ⇒ 
  ∀P: Type[1].
  (∀e0: (eq A (R0 ? t0) u0).
   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].

nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
#A;#B;#x;#y;#e;nrewrite > e;ncases y;
#a;#b;nnormalize;#P;#PH;napply PH;@;
nqed.

nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
napply pos_elim; /3/;
nqed.

nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
napply pos_elim;
##[ //
##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
##] nqed.

ntheorem plus_minus_r:
∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
#m;#n;#p;#le;nrewrite > (symmetric_plus …);
nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.

nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
#m;#n;#p;nelim m;/2/; nqed.
(*
nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
#m;#n;nelim n;
##[ nrewrite < (minus_n_O …); /2/;
##| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct;
    nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
##] nqed.
*)
nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
#n;#m;#p;(*nelim (decidable_lt n m);*)#lt;
(*##[*) napply (pos_elim … p); //;#p'; #IH;
    nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
    nrewrite > (minus_plus_distrib …);
    nrewrite < (plus_minus … lt); nrewrite < IH;
    nrewrite > (plus_minus_r …); /2/;
nqed.
(*##|
nlapply (not_lt_to_le … lt); #le;
napply (pos_elim … p); //; #p';
 ncut (m-n = one); ##[ /3/ ##]
  #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
  #H; nrewrite < H in ⊢ (???%); 
  napply sym_eq; napply  le_n_one_to_eq; nrewrite < H;
  nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
  /2/;
##] nqed.

nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
#m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//;
#H'; nlapply (minus_to_plus … H'); /2/;
nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H;
napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
nqed.
*)

nlet rec natp_plus (n,m:natp) ≝
match n with
[ pzero ⇒ m
| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
].

nlet rec natp_times (n,m:natp) ≝
match n with
[ pzero ⇒ pzero
| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
].

ninductive natp_lt : natp → Pos → Prop ≝
| plt_zero : ∀n. natp_lt pzero n
| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.

nlemma lt_p0: ∀n:Pos. one < p0 n.
#n; nnormalize; /2/; nqed.

nlemma lt_p1: ∀n:Pos. one < p1 n.
#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.

nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
#m; nelim m;
##[ //;
##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
##] nqed.

nlemma pos_nonzero2: ∀n. ∀P:Pos→Type. ∀Q:Type. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n).
#n P Q; napply succ_elim; /2/; nqed.

nlemma partial_minus_to_Prop: ∀n,m.
  match partial_minus n m with
  [ MinusNeg ⇒ n < m
  | MinusZero ⇒ n = m
  | MinusPos r ⇒ n = m+r
  ].
#n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
nnormalize; ncases (partial_minus n m); /2/; nqed.

nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
#n m lt; nelim lt; /2/;
nqed.

nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
nqed.

nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
#n m lt; ninversion lt;
##[ #H; nrewrite > (succ_injective … H); //;
##| #p H1 H2 H3;nrewrite > (succ_injective … H3);
    napply (transitive_lt ? (p0 p) ?); /2/;
##] 
nqed.

nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
#n m lt; nelim lt; /2/;
nqed.



nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
#n m lt;ninversion lt;
##[ #p H; ndestruct;
##| #n' m' lt e1 e2; ndestruct; //;
##] nqed.

nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
#a b; /2/; nqed.

nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.

nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
/2/; nqed.

nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
#A B a1 a2 b1 b2 H; ndestruct; //;
nqed.

nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
#A B a1 a2 b1 b2 H; ndestruct; //;
nqed.

ntheorem divide_ok : ∀m,n,dv,md.
 divide m n = 〈dv,md〉 →
 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
#m n; napply (pos_cases … n);
##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
##| #n'; nelim m;
  ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
  ##| #m' IH dv md; nnormalize;
      nlapply (refl ? (divide m' (succ n')));
      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
      #dv' md' DIVr; nelim (IH … DIVr);
      nnormalize; ncases md';
      ##[ ncases dv'; nnormalize;
        ##[ #H; ndestruct;
        ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
        ##]
      ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
          nnormalize; #n md'' Hr1 Hr2;
          nlapply (plt_lt … Hr2); #Hr2';
          nlapply (partial_minus_to_Prop md'' n);
          ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
          #lt; #e; ndestruct; @; /2/; napply plt_pos;
          ##[ ##1,3,5,7: napply double_lt1; /2/;
          ##| ##2,4: napply double_lt3; /2/;
          ##| ##*: napply double_lt2; /2/;
          ##]
      ##]
  ##| #m' IH dv md; nwhd in ⊢ (??%? → ?);
      nlapply (refl ? (divide m' (succ n')));
      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
      #dv' md' DIVr; nelim (IH … DIVr);
      nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
      ##[ ncases dv'; nnormalize;
        ##[ #H; ndestruct;
        ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
        ##]
      ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
          nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
          nlapply (plt_lt … Hr2); #Hr2';
          nwhd in ⊢ (??%? → ?);
          nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
          ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]
          ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
          #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
          #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
          nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e);
          nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
          ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
          ##| ncut (succ n' + r'' < p0 (succ n')); /2/;
          ##| /2/;
          ##| /2/;
          ##]
      ##]
  ##]
##] nqed.

nlemma mod0_divides: ∀m,n,dv:Pos.
  divide n m = 〈ppos dv,pzero〉 → m∣n.
#m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
nnormalize; #H; ndestruct; //;
nqed.

nlemma divides_mod0: ∀dv,m,n:Pos.
  n = dv*m → divide n m = 〈ppos dv,pzero〉.
#dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
nlapply (divide_ok … DIVIDE); *;
ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
##[ nlapply (plus_to_minus … e0);
    nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
    ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;
    nrewrite > (minus_times_distrib_l …); //;

 (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
    #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
    napply (absurd ? B (lt_to_not_le … A));

##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;

##| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
##]
nqed.

nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
#m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
#dv;#md; ncases md; ncases dv;
##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
##| #dv'; #H; @1; napply mod0_divides; /2/;
##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
    nrewrite > DIVIDES; #H'; 
    ndestruct;
##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
    nrewrite > DIVIDES; #H'; 
    ndestruct;
##] nqed.

ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
#p;#q;ncases p;
##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##]
##| ##*: #n; ncases q; nnormalize; /2/;
##] nqed.

ndefinition natp_to_Z ≝
λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].

ndefinition natp_to_negZ ≝
λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].

(* TODO: check these definitions are right.  They are supposed to be the same
   as Zdiv/Zmod in Coq. *)
ndefinition divZ ≝ λx,y.
  match x with
  [ OZ ⇒ OZ
  | pos n ⇒
    match y with
    [ OZ ⇒ OZ
    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
    ]
  | neg n ⇒
    match y with
    [ OZ ⇒ OZ
    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
    ]
  ].

ndefinition modZ ≝ λx,y.
  match x with
  [ OZ ⇒ OZ
  | pos n ⇒
    match y with
    [ OZ ⇒ OZ
    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
    ]
  | neg n ⇒
    match y with
    [ OZ ⇒ OZ
    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    ]
  ].

interpretation "natural division" 'divide m n = (div m n).
interpretation "natural modulus" 'module m n = (mod m n).
interpretation "integer division" 'divide m n = (divZ m n).
interpretation "integer modulus" 'module m n = (modZ m n).

nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
#x y; ncases y;
##[ #H; napply (False_ind … H);
##| #m; #_; ncases x; //; #n;
    nwhd in ⊢ (?%?);
    nlapply (pos_compare_to_Prop n m);
    ncases (pos_compare n m); /2/;
    #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
##| #m H; napply (False_ind … H);
##] nqed.

nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
#n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
##[ //;
##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
##] nqed.

ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
#x y; ncases y;
##[ #H; napply (False_ind … H);
##| #m; #_; ncases x;
  ##[ @;//;
  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
      ncases (divide n m) in ⊢ (???% → %); #dv md H;
      nelim (divide_ok … H); #e l; nelim l; /2/;
  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
      ncases (divide n m) in ⊢ (???% → %); #dv md H;
      nelim (divide_ok … H); #e l; nelim l;
      ##[ /2/;
      ##| #md' m' l'; @;
        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
            nrewrite > (pos_compare_lt … l'); //;
        ##| napply Zminus_Zlt; //;
        ##]
      ##]
  ##]
##| #m H; napply (False_ind … H);
##] nqed.