Added theorems; created NZPlusOrder from NTimesOrder.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10325 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 35 insertions, 4 deletions

diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index bcef668677..956eca896c 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -45,6 +45,15 @@ Proof NZpred_succ.
 Theorem pred_0 : P 0 == 0.
 Proof pred_0.
 
+Theorem Neq_refl : forall n : N, n == n.
+Proof (proj1 NZeq_equiv).
+
+Theorem Neq_symm : forall n m : N, n == m -> m == n.
+Proof (proj2 (proj2 NZeq_equiv)).
+
+Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p.
+Proof (proj1 (proj2 NZeq_equiv)).
+
 Theorem neq_symm : forall n m : N, n ~= m -> m ~= n.
 Proof NZneq_symm.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 33214cd1bf..c7b7d495f7 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -80,6 +80,12 @@ Proof NZlt_succ_diag_r.
 Theorem le_succ_diag_r : forall n : N, n <= S n.
 Proof NZle_succ_diag_r.
 
+Theorem lt_0_1 : 0 < 1.
+Proof NZlt_0_1.
+
+Theorem le_0_1 : 0 <= 1.
+Proof NZle_0_1.
+
 Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m.
 Proof NZlt_lt_succ_r.
 
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index d6c0bfafa1..502f994174 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -56,6 +56,20 @@ Proof NZeq_times_0_l.
 Theorem eq_times_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0.
 Proof NZeq_times_0_r.
 
+Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m.
+Proof.
+intros n m; split; intro;
+[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg];
+try assumption; apply le_0_l.
+Qed.
+
+Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m.
+Proof.
+intros n m; split; intro;
+[apply NZsquare_le_mono_nonneg | apply NZsquare_le_simpl_nonneg];
+try assumption; apply le_0_l.
+Qed.
+
 Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof NZtimes_2_mono_l.
 
@@ -73,21 +87,23 @@ Qed.
 
 Theorem times_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q.
 Proof.
-intros; apply NZtimes_lt_mono; try assumption; apply le_0_l.
+intros; apply NZtimes_lt_mono_nonneg; try assumption; apply le_0_l.
 Qed.
 
 Theorem times_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q.
 Proof.
-intros; apply NZtimes_le_mono; try assumption; apply le_0_l.
+intros; apply NZtimes_le_mono_nonneg; try assumption; apply le_0_l.
 Qed.
 
-Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
+Theorem lt_0_times : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
-apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
+apply -> NZlt_0_times in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
 now apply NZtimes_pos_pos.
 Qed.
 
+Notation times_pos := lt_0_times (only parsing).
+
 Theorem eq_times_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1.
 Proof.
 intros n m.