Require Export NArith.
Require Import ZArith.

Open Scope N_scope.

Theorem Nle_le: forall n  m, (N.to_nat n <= N.to_nat m)%nat -> n <= m.
(* Goal: forall (n m : N) (_ : le (N.to_nat n) (N.to_nat m)), N.le n m *)
intros n m; case n; case m; unfold N.le; simpl; try (intros; discriminate).
(* Goal: forall (p : positive) (_ : ge O (Pos.to_nat p)), not (@eq comparison Lt Lt) *)
(* Goal: forall (p p0 : positive) (_ : ge (Pos.to_nat p0) (Pos.to_nat p)), not (@eq comparison (Pos.compare p0 p) Lt) *)
intros p; elim p using Pind; simpl.
(* Goal: forall _ : gt O O, @eq comparison Eq Gt *)
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros H1; inversion H1. 
(* Goal: forall (p : positive) (_ : forall _ : ge O (Pos.to_nat p), not (@eq comparison Lt Lt)) (_ : ge O (Pos.to_nat (Pos.succ p))), not (@eq comparison Lt Lt) *)
(* Goal: forall (p p0 : positive) (_ : ge (Pos.to_nat p0) (Pos.to_nat p)), not (@eq comparison (Pos.compare p0 p) Lt) *)
intros n1 _; rewrite nat_of_P_succ_morphism.
(* Goal: forall _ : gt O O, @eq comparison Eq Gt *)
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros H1; inversion H1.
(* Goal: forall (p p0 : positive) (_ : le (Pos.to_nat p0) (Pos.to_nat p)), not (@eq comparison (Pos.compare p0 p) Gt) *)
intros p1 p2 H1 H2; absurd (nat_of_P p2 > nat_of_P p1)%nat; auto with arith.
(* Goal: gt (Pos.to_nat p2) (Pos.to_nat p1) *)
apply nat_of_P_gt_Gt_compare_morphism; auto.
Qed.

Theorem le_Nle: forall n m, N.of_nat n <= N.of_nat m -> (n <= m)%nat.
(* Goal: forall (n m : nat) (_ : N.le (N.of_nat n) (N.of_nat m)), le n m *)
intros n m; case n; case m; unfold N.le; simpl; auto with arith.
(* Goal: forall (n : nat) (_ : not (@eq comparison Lt Lt)), ge O (S n) *)
(* Goal: forall (n n0 : nat) (_ : not (@eq comparison (Pos.compare (Pos.of_succ_nat n0) (Pos.of_succ_nat n)) Lt)), ge (S n0) (S n) *)
intros n1 H1; case H1; auto.
(* Goal: forall (n n0 : nat) (_ : not (@eq comparison (Pos.compare (Pos.of_succ_nat n0) (Pos.of_succ_nat n)) Gt)), le (S n0) (S n) *)
intros m1 n1 H1; case (le_or_lt n1 m1); auto with arith.
(* Goal: forall _ : lt n1 m1, ge (S n1) (S m1) *)
intros H2; case H1.
(* Goal: @eq comparison (Pos.compare (Pos.of_succ_nat n1) (Pos.of_succ_nat m1)) Gt *)
apply nat_of_P_gt_Gt_compare_complement_morphism.
repeat rewrite  nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith.
Qed.

Theorem Nle_le_rev: forall n  m, n <= m -> (N.to_nat n <= N.to_nat m)%nat.
(* Goal: forall (n m : N) (_ : N.le n m), le (N.to_nat n) (N.to_nat m) *)
intros; apply le_Nle; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nlt_lt: forall n  m, (N.to_nat n < N.to_nat m)%nat -> n < m.
(* Goal: forall (n m : N) (_ : lt (N.to_nat n) (N.to_nat m)), N.lt n m *)
intros n m; case n; case m; unfold N.lt; simpl; try (intros; discriminate); auto.
(* Goal: forall _ : gt O O, @eq comparison Eq Gt *)
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros H1; inversion H1.
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros p H1; inversion H1.
(* Goal: forall (p p0 : positive) (_ : lt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Lt *)
intros; apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
Qed.

Theorem lt_Nlt: forall n m, N.of_nat n < N.of_nat m -> (n < m)%nat.
(* Goal: forall (n m : nat) (_ : N.lt (N.of_nat n) (N.of_nat m)), lt n m *)
intros n m; case n; case m; unfold N.lt; simpl; try (intros; discriminate); auto with arith.
(* Goal: forall (n n0 : nat) (_ : @eq comparison (Pos.compare (Pos.of_succ_nat n0) (Pos.of_succ_nat n)) Gt), gt (S n0) (S n) *)
intros m1 n1 H1.
(* Goal: gt (S n1) (S m1) *)
rewrite <- (Nat2N.id (S n1)); rewrite <- (Nat2N.id (S m1)).
(* Goal: lt (N.to_nat (N.of_nat (S n1))) (N.to_nat (N.of_nat (S m1))) *)
simpl; apply nat_of_P_lt_Lt_compare_morphism; auto.
Qed.

Theorem Nlt_lt_rev: forall n  m, n < m -> (N.to_nat n < N.to_nat m)%nat.
(* Goal: forall (n m : N) (_ : N.lt n m), lt (N.to_nat n) (N.to_nat m) *)
intros; apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.


Theorem Nge_ge: forall n  m, (N.to_nat n >= N.to_nat m)%nat -> n >= m.
(* Goal: forall (n m : N) (_ : ge (N.to_nat n) (N.to_nat m)), N.ge n m *)
intros n m; case n; case m; unfold N.ge; simpl; try (intros; discriminate); auto.
(* Goal: forall (p : positive) (_ : ge O (Pos.to_nat p)), not (@eq comparison Lt Lt) *)
(* Goal: forall (p p0 : positive) (_ : ge (Pos.to_nat p0) (Pos.to_nat p)), not (@eq comparison (Pos.compare p0 p) Lt) *)
intros p; elim p using Pind; simpl.
(* Goal: forall _ : gt O O, @eq comparison Eq Gt *)
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros H1; inversion H1. 
(* Goal: forall (p : positive) (_ : forall _ : ge O (Pos.to_nat p), not (@eq comparison Lt Lt)) (_ : ge O (Pos.to_nat (Pos.succ p))), not (@eq comparison Lt Lt) *)
(* Goal: forall (p p0 : positive) (_ : ge (Pos.to_nat p0) (Pos.to_nat p)), not (@eq comparison (Pos.compare p0 p) Lt) *)
intros n1 _; rewrite nat_of_P_succ_morphism.
(* Goal: forall _ : gt O O, @eq comparison Eq Gt *)
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros H1; inversion H1.
(* Goal: forall (p p0 : positive) (_ : ge (Pos.to_nat p0) (Pos.to_nat p)), not (@eq comparison (Pos.compare p0 p) Lt) *)
intros p1 p2 H1 H2; absurd (nat_of_P p2 < nat_of_P p1)%nat; auto with arith.
(* Goal: lt (Pos.to_nat p2) (Pos.to_nat p1) *)
apply nat_of_P_lt_Lt_compare_morphism; auto.
Qed.

Theorem ge_Nge: forall n m, N.of_nat n >= N.of_nat m -> (n >= m)%nat.
(* Goal: forall (n m : nat) (_ : N.ge (N.of_nat n) (N.of_nat m)), ge n m *)
intros n m; case n; case m; unfold N.ge; simpl; try (intros; discriminate); auto with arith.
(* Goal: forall (n : nat) (_ : not (@eq comparison Lt Lt)), ge O (S n) *)
(* Goal: forall (n n0 : nat) (_ : not (@eq comparison (Pos.compare (Pos.of_succ_nat n0) (Pos.of_succ_nat n)) Lt)), ge (S n0) (S n) *)
intros n1 H1; case H1; auto.
(* Goal: forall (n n0 : nat) (_ : @eq comparison (Pos.compare (Pos.of_succ_nat n0) (Pos.of_succ_nat n)) Gt), gt (S n0) (S n) *)
intros m1 n1 H1.
(* Goal: ge (S n1) (S m1) *)
case (le_or_lt m1 n1); auto with arith.
(* Goal: forall _ : lt n1 m1, ge (S n1) (S m1) *)
intros H2; case H1.
(* Goal: @eq comparison (Pos.compare (Pos.of_succ_nat n1) (Pos.of_succ_nat m1)) Lt *)
apply nat_of_P_lt_Lt_compare_complement_morphism.
repeat rewrite  nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith.
Qed.

Theorem Nge_ge_rev: forall n  m, n >= m -> (N.to_nat n >= N.to_nat m)%nat.
(* Goal: forall (n m : N) (_ : N.ge n m), ge (N.to_nat n) (N.to_nat m) *)
intros; apply ge_Nge; repeat rewrite N2Nat.id; auto.
Qed.


Theorem Ngt_gt: forall n  m, (N.to_nat n > N.to_nat m)%nat -> n > m.
(* Goal: forall (n m : N) (_ : gt (N.to_nat n) (N.to_nat m)), N.gt n m *)
intros n m; case n; case m; unfold N.gt; simpl; try (intros; discriminate); auto.
(* Goal: forall _ : gt O O, @eq comparison Eq Gt *)
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros H1; inversion H1.
(* Goal: forall (p : positive) (_ : gt O (Pos.to_nat p)), @eq comparison Lt Gt *)
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros p H1; inversion H1.
(* Goal: forall (p p0 : positive) (_ : gt (Pos.to_nat p0) (Pos.to_nat p)), @eq comparison (Pos.compare p0 p) Gt *)
intros; apply nat_of_P_gt_Gt_compare_complement_morphism; auto.
Qed.

Theorem gt_Ngt: forall n m, N.of_nat n > N.of_nat m -> (n > m)%nat.
(* Goal: forall (n m : nat) (_ : N.gt (N.of_nat n) (N.of_nat m)), gt n m *)
intros n m; case n; case m; unfold N.gt; simpl; try (intros; discriminate); auto with arith.
(* Goal: forall (n n0 : nat) (_ : @eq comparison (Pos.compare (Pos.of_succ_nat n0) (Pos.of_succ_nat n)) Gt), gt (S n0) (S n) *)
intros m1 n1 H1.
(* Goal: gt (S n1) (S m1) *)
rewrite <- (Nat2N.id (S n1)); rewrite <- (Nat2N.id (S m1)).
(* Goal: gt (Pos.to_nat p2) (Pos.to_nat p1) *)
simpl; apply nat_of_P_gt_Gt_compare_morphism; auto.
Qed.

Theorem Ngt_gt_rev: forall n  m, n > m -> (N.to_nat n > N.to_nat m)%nat.
(* Goal: forall (n m : N) (_ : N.gt n m), gt (N.to_nat n) (N.to_nat m) *)
intros; apply gt_Ngt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Neq_eq_rev: forall n  m, n = m -> (N.to_nat n = N.to_nat m)%nat.
(* Goal: forall (n m : N) (_ : @eq N n m), @eq nat (N.to_nat n) (N.to_nat m) *)
intros n m H; rewrite H; auto.
Qed.

Import BinPos.


Ltac to_nat_op  :=
  match goal with
      H: (N.lt _ _) |- _ => generalize (Nlt_lt_rev _ _ H); clear H; intros H
|     H: (N.gt _ _) |- _ => generalize (Ngt_gt_rev _ _ H); clear H; intros H
|     H: (N.le _ _) |- _ => generalize (Nle_le_rev _ _ H); clear H; intros H
|     H: (N.ge _ _) |- _ => generalize (Nge_ge_rev _ _ H); clear H; intros H
|     H: (@eq N _ _) |- _ => generalize (Neq_eq_rev _ _ H); clear H; intros H
|      |- (N.lt _ _)  => apply Nlt_lt
|      |- (N.le _ _)  => apply Nle_le
|      |- (N.gt _ _)  => apply Ngt_gt
|      |- (N.ge _ _)  => apply Nge_ge
|      |- (@eq N _ _)  => apply Nat2N.inj
end.

Ltac set_to_nat :=
let nn := fresh "nn" in
match goal with
       |- context [(N.to_nat (?X + ?Y)%N)]  => rewrite N2Nat.inj_add
|      |- context [(N.to_nat (?X * ?Y)%N)]  => rewrite N2Nat.inj_mul
|      |- context [(N.to_nat ?X)]  => set (nn:=N.to_nat X) in * |- *
|      H: context [(N.to_nat (?X + ?Y)%N)] |- _ => rewrite N2Nat.inj_add in H
|      H: context [(N.to_nat (?X + ?Y)%N)] |- _ => rewrite N2Nat.inj_mul in H
|      H: context [(N.to_nat ?X)] |- _ => set (nn:=N.to_nat X) in * |- *
end.

Ltac to_nat := repeat to_nat_op; repeat set_to_nat.

Theorem Nle_gt_trans: forall n m p, m <= n -> m > p -> n > p.
(* Goal: forall (n m p : N) (_ : N.le m n) (_ : N.gt m p), N.gt n p *)
intros; to_nat; apply le_gt_trans with nn1; auto.
Qed.

Theorem Ngt_le_trans: forall n m p, n > m -> p <= m -> n > p.
(* Goal: forall (n m p : N) (_ : N.gt n m) (_ : N.le p m), N.gt n p *)
intros; to_nat; apply gt_le_trans with nn1; auto.
Qed.

Theorem Nle_add_l :
  forall x y, x <= y + x.
(* Goal: forall x y : N, N.le x (N.add y x) *)
intros; to_nat; auto with arith.
Qed.

Close Scope N_scope.
