OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith

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

1 files changed, 19 insertions, 0 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index d9d848f0d..eaf3f126a 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -383,11 +383,30 @@ destruct n; destruct m; simpl; auto.
 exact (Pcompare_antisym p p0 Eq).
 Qed.
 
+Lemma Ngt_Nlt : forall n m, n > m -> m < n.
+Proof.
+unfold Ngt, Nlt; intros n m GT.
+rewrite <- Ncompare_antisym, GT; reflexivity.
+Qed.
+
 Theorem Nlt_irrefl : forall n : N, ~ n < n.
 Proof.
 intro n; unfold Nlt; now rewrite Ncompare_refl.
 Qed.
 
+Theorem Nlt_trans : forall n m q, n < m -> m < q -> n < q.
+Proof.
+destruct n;
+ destruct m; try discriminate;
+ destruct q; try discriminate; auto.
+eapply Plt_trans; eauto.
+Qed.
+
+Theorem Nlt_not_eq : forall n m, n < m -> ~ n = m.
+Proof.
+ intros n m LT EQ. subst m. elim (Nlt_irrefl n); auto.
+Qed.
+
 Theorem Ncompare_n_Sm :
   forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m.
 Proof.