(* Ugly tacty to resolve sign condition for N *)
Require Import NatSignTac.
Require Import NAux.
Require Import NArith.
Require Import List.
Require Export NGroundTac.

Open Scope N_scope.

Theorem Nmult_lt_compat_l: forall n m p, n < m -> 0 < p -> p * n < p * m.
(* Goal: forall (n m p : N) (_ : N.lt n m) (_ : N.lt N0 p), N.lt (N.mul p n) (N.mul p m) *)
intros n m p H1 H2; apply Nlt_lt; repeat rewrite N2Nat.inj_mul.
(* Goal: lt (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
apply mult_lt_compat_l; apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_le_compat_l: forall n m p, n <= m -> p * n <= p * m.
(* Goal: forall (n m p : N) (_ : N.le n m), N.le (N.mul p n) (N.mul p m) *)
intros n m p H1; apply Nle_le; repeat rewrite N2Nat.inj_mul.
(* Goal: le (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
apply Mult.mult_le_compat_l; apply le_Nle; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_ge_compat_l: forall n m p, n >= m -> p * n >= p * m.
(* Goal: forall (n m p : N) (_ : N.ge n m), N.ge (N.mul p n) (N.mul p m) *)
intros n m p H1; apply Nge_ge; repeat rewrite N2Nat.inj_mul.
(* Goal: ge (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
apply mult_ge_compat_l; apply ge_Nge; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_gt_compat_l: forall n m p, n > m -> p > 0 -> p * n > p * m.
(* Goal: forall (n m p : N) (_ : N.gt n m) (_ : N.gt p N0), N.gt (N.mul p n) (N.mul p m) *)
intros n m p H1 H2; apply Ngt_gt; repeat rewrite N2Nat.inj_mul.
(* Goal: gt (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
apply mult_gt_compat_l; apply gt_Ngt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_lt_compat_rev_l1: forall n m p, p * n < p * m -> 0 < p.
(* Goal: forall (n m p : N) (_ : N.lt (N.mul p n) (N.mul p m)), N.lt N0 p *)
intros n m p H1; apply Nlt_lt; apply mult_lt_compat_rev_l1 with (nat_of_N n) (nat_of_N m).
(* Goal: lt (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
repeat rewrite <- N2Nat.inj_mul; apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_lt_compat_rev_l2: forall n m p, p * n < p * m -> n < m.
(* Goal: forall (n m p : N) (_ : N.lt (N.mul p n) (N.mul p m)), N.lt n m *)
intros n m p H1; apply Nlt_lt; apply mult_lt_compat_rev_l2 with (nat_of_N p).
(* Goal: lt (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
repeat rewrite <- N2Nat.inj_mul; apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_gt_compat_rev_l1: forall n m p, p * n > p * m -> p > 0.
(* Goal: forall (n m p : N) (_ : N.gt (N.mul p n) (N.mul p m)), N.gt p N0 *)
intros n m p H1; apply Ngt_gt; apply mult_gt_compat_rev_l1 with (nat_of_N n) (nat_of_N m).
(* Goal: gt (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
repeat rewrite <- N2Nat.inj_mul; apply gt_Ngt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_gt_compat_rev_l2: forall n m p, p * n > p * m -> n > m.
(* Goal: forall (n m p : N) (_ : N.gt (N.mul p n) (N.mul p m)), N.gt n m *)
intros n m p H1; apply Ngt_gt; apply mult_gt_compat_rev_l2 with (nat_of_N p).
(* Goal: gt (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
repeat rewrite <- N2Nat.inj_mul; apply gt_Ngt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_le_compat_rev_l: forall n m p, p * n <= p * m -> 0 < p -> n <= m.
(* Goal: forall (n m p : N) (_ : N.le (N.mul p n) (N.mul p m)) (_ : N.lt N0 p), N.le n m *)
intros n m p H1 H2; apply Nle_le; apply mult_le_compat_rev_l with (nat_of_N p). 
(* Goal: le (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
(* Goal: lt O (N.to_nat p) *)
repeat rewrite <- N2Nat.inj_mul; apply le_Nle; repeat rewrite N2Nat.id; auto.
(* Goal: lt O (N.to_nat p) *)
apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nmult_ge_compat_rev_l: forall n m p , p * n >= p * m -> 0 < p -> n >= m.
(* Goal: forall (n m p : N) (_ : N.ge (N.mul p n) (N.mul p m)) (_ : N.lt N0 p), N.ge n m *)
intros n m p H1 H2; apply Nge_ge; apply mult_ge_compat_rev_l with (nat_of_N p). 
(* Goal: ge (Nat.mul (N.to_nat p) (N.to_nat n)) (Nat.mul (N.to_nat p) (N.to_nat m)) *)
(* Goal: lt O (N.to_nat p) *)
repeat rewrite <- N2Nat.inj_mul; apply ge_Nge; repeat rewrite N2Nat.id; auto.
(* Goal: lt O (N.to_nat p) *)
apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nlt_mult_0: forall a b, 0 < a -> 0 < b -> 0 < a * b.
(* Goal: lt O (N.to_nat p) *)
intros a b H1 H2; apply Nlt_lt; rewrite N2Nat.inj_mul; apply lt_mult_0; apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Ngt_mult_0: forall a b, a > 0 -> b > 0 -> a * b > 0.
(* Goal: forall (a b : N) (_ : N.gt a N0) (_ : N.gt b N0), N.gt (N.mul a b) N0 *)
intros a b H1 H2; apply Ngt_gt; rewrite N2Nat.inj_mul; apply gt_mult_0; apply gt_Ngt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nlt_mult_rev_0_l: forall a b, 0 < a * b ->  0 < a .
(* Goal: forall (a b : N) (_ : N.lt N0 (N.mul a b)), N.lt N0 a *)
intros a b H1; apply Nlt_lt; apply lt_mult_rev_0_l with (nat_of_N b). 
(* Goal: lt O (N.to_nat p) *)
rewrite <- N2Nat.inj_mul; apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nlt_mult_rev_0_r: forall a b, 0 < a * b ->  0 < b .
(* Goal: forall (a b : N) (_ : N.lt N0 (N.mul a b)), N.lt N0 b *)
intros a b H1; apply Nlt_lt; apply lt_mult_rev_0_r with (nat_of_N a). 
(* Goal: lt O (N.to_nat p) *)
rewrite <- N2Nat.inj_mul; apply lt_Nlt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Ngt_mult_rev_0_l: forall a b, a * b > 0 ->  a > 0.
(* Goal: forall (a b : N) (_ : N.gt (N.mul a b) N0), N.gt a N0 *)
intros a b H1; apply Ngt_gt; apply gt_mult_rev_0_l with (nat_of_N b). 
(* Goal: gt (Nat.mul (N.to_nat a) (N.to_nat b)) O *)
rewrite <- N2Nat.inj_mul; apply gt_Ngt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Ngt_mult_rev_0_r: forall a b, a * b > 0  ->  b > 0 .
(* Goal: forall (a b : N) (_ : N.gt (N.mul a b) N0), N.gt b N0 *)
intros a b H1; apply Ngt_gt; apply gt_mult_rev_0_r with (nat_of_N a). 
(* Goal: gt (Nat.mul (N.to_nat a) (N.to_nat b)) O *)
rewrite <- N2Nat.inj_mul; apply gt_Ngt; repeat rewrite N2Nat.id; auto.
Qed.

Theorem Nle_0_eq_0: forall n, n <= 0 -> n = 0.
(* Goal: forall (n : N) (_ : N.ge N0 n), @eq N n N0 *)
intros n H1; rewrite <- (N2Nat.id n).
(* Goal: @eq N (N.of_nat (N.to_nat n)) N0 *)
rewrite (le_0_eq_0 (nat_of_N n)); auto.
(* Goal: le (N.to_nat n) O *)
apply le_Nle; rewrite N2Nat.id; auto.
Qed.

Theorem Nge_0_eq_0: forall n, 0 >= n -> n = 0.
(* Goal: forall (n : N) (_ : N.ge N0 n), @eq N n N0 *)
intros n H1; rewrite <- (N2Nat.id n).
(* Goal: @eq N (N.of_nat (N.to_nat n)) N0 *)
rewrite (le_0_eq_0 (nat_of_N n)); auto.
(* Goal: le (N.to_nat n) O *)
change (0 >= nat_of_N n)%nat.
(* Goal: ge O (N.to_nat n) *)
apply ge_Nge; rewrite N2Nat.id; auto.
Qed.

Ltac Nsign_tac :=
 repeat (apply Nmult_le_compat_l || apply Nmult_lt_compat_l ||
              apply Nmult_ge_compat_l || apply Nmult_gt_compat_l ||
              apply Nlt_mult_0 || apply Ngt_mult_0); auto.

Ltac hyp_Nsign_tac H :=
  match type of H with
   0 <= _ => clear H
| (?X1 <= 0)%N => generalize (Nle_0_eq_0 _ H); clear H; intros H; subst X1
|  (?X1 * _ <= ?X1 * _)%N => 
             let s1 := fresh "NS" in
                   (assert (s1: 0 < X1); [Nsign_tac; fail |
                   generalize (Nmult_le_compat_rev_l _ _ _ H s1);
                   clear H s1; intros H])
|   (0  < ?X1 * _)%N  => 
              let s1 := fresh "NS" in
                   (generalize (Nlt_mult_rev_0_l _ _ H);
                    generalize (Nlt_mult_rev_0_r _ _ H); clear H;
                    intros H s1; hyp_Nsign_tac s1; hyp_Nsign_tac H)
|  (?X1 < 0)%N => absurd (~ (X1 < 0)%N); auto
| (?X1 * _  < ?X1 * _)%N => 
              let s1 := fresh "NS" in
                   (generalize (Nmult_lt_compat_rev_l1 _ _ _ H);
                    generalize (Nmult_lt_compat_rev_l2 _ _ _ H); clear H;
                    intros H s1; hyp_Nsign_tac s1; hyp_Nsign_tac H)
|  (?X1 >= 0)%N => clear H
| (0 >= ?X1)%N  => generalize (Nge_0_eq_0 _ H); clear H; intros H; subst X1
|  (?X1 * _ >= ?X1 * _)%N => 
             let s1 := fresh "NS" in
                   (assert (s1: (0 < X1)%N); [Nsign_tac; fail |
                   generalize (Nmult_ge_compat_rev_l _ _ _ H s1);
                   clear H s1; intros H])
|  (?X1 * _ > 0 )%N => 
              let s1 := fresh "NS" in
                   (generalize (Ngt_mult_rev_0_l _ _ H);
                    generalize (Ngt_mult_rev_0_r _ _ H); clear H;
                    intros H s1; hyp_Nsign_tac s1; hyp_Nsign_tac H)
|  (0 > ?X1)%N => absurd (~ (0 > X1)%N); auto with arith
| (?X1 * _  > ?X1 * _)%N => 
              let s1 := fresh "NS" in
                   (generalize (Nmult_gt_compat_rev_l1 _ _ _ H);
                    generalize (Nmult_gt_compat_rev_l2 _ _ _ H); clear H;
                    intros H s1; hyp_Nsign_tac s1; hyp_Nsign_tac H)
  |  _ => (let u := type of H in (clear H; assert (H: u); [auto; fail | clear H]) || idtac)
              
   end.

Close Scope N_scope.