2 files changed, 47 insertions, 4 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 5aa397f8a..1e3ab6687 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1367,7 +1367,7 @@ Lemma inj_testbit a n : 0<=n ->
  Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
 Proof. apply Z.testbit_Zpos. Qed.
 
-(** Some results concerning Z.neg *)
+(** Some results concerning Z.neg and Z.pos *)
 
 Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q.
 Proof. now injection 1. Qed.
@@ -1375,18 +1375,54 @@ Proof. now injection 1. Qed.
 Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q.
 Proof. split. apply inj_neg. intros; now f_equal. Qed.
 
+Lemma inj_pos p q : Z.pos p = Z.pos q -> p = q.
+Proof. now injection 1. Qed.
+
+Lemma inj_pos_iff p q : Z.pos p = Z.pos q <-> p = q.
+Proof. split. apply inj_pos. intros; now f_equal. Qed.
+
 Lemma neg_is_neg p : Z.neg p < 0.
 Proof. reflexivity. Qed.
 
 Lemma neg_is_nonpos p : Z.neg p <= 0.
 Proof. easy. Qed.
 
+Lemma pos_is_pos p : 0 < Z.pos p.
+Proof. reflexivity. Qed.
+
+Lemma pos_is_nonneg p : 0 <= Z.pos p.
+Proof. easy. Qed.
+
+Lemma neg_le_pos p q : Zneg p <= Zpos q.
+Proof. easy. Qed.
+
+Lemma neg_lt_pos p q : Zneg p < Zpos q.
+Proof. easy. Qed.
+
+Lemma neg_le_neg p q : (q <= p)%positive -> Zneg p <= Zneg q.
+Proof. intros; unfold Z.le; simpl. now rewrite <- Pos.compare_antisym. Qed.
+
+Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q.
+Proof. intros; unfold Z.lt; simpl. now rewrite <- Pos.compare_antisym. Qed.
+
+Lemma pos_le_pos p q : (p <= q)%positive -> Zpos p <= Zpos q.
+Proof. easy. Qed.
+
+Lemma pos_lt_pos p q : (p < q)%positive -> Zpos p < Zpos q.
+Proof. easy. Qed.
+
 Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p.
 Proof. reflexivity. Qed.
 
 Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1.
 Proof. reflexivity. Qed.
 
+Lemma pos_xO p : Z.pos p~0 = 2 * Z.pos p.
+Proof. reflexivity. Qed.
+
+Lemma pos_xI p : Z.pos p~1 = 2 * Z.pos p + 1.
+Proof. reflexivity. Qed.
+
 Lemma opp_neg p : - Z.neg p = Z.pos p.
 Proof. reflexivity. Qed.
 
@@ -1402,6 +1438,9 @@ Proof. reflexivity. Qed.
 Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p.
 Proof. reflexivity. Qed.
 
+Lemma add_pos_pos p q : Z.pos p + Z.pos q = Z.pos (p+q).
+Proof. reflexivity. Qed.
+
 Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p).
 Proof. apply Z.divide_Zpos_Zneg_r. Qed.
 
@@ -1412,6 +1451,10 @@ Lemma testbit_neg a n : 0<=n ->
  Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)).
 Proof. apply Z.testbit_Zneg. Qed.
 
+Lemma testbit_pos a n : 0<=n ->
+ Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
+Proof. apply Z.testbit_Zpos. Qed.
+
 End Pos2Z.
 
 Module Z2Pos.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 73dee0cf2..18915216a 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -339,7 +339,7 @@ Notation Zle_0_1 := Z.le_0_1 (compat "8.3").
 
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
-  easy.
+  exact Pos2Z.neg_le_pos.
 Qed.
 
 Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0.
@@ -350,12 +350,12 @@ Qed.
 (* weaker but useful (in [Z.pow] for instance) *)
 Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p.
 Proof.
- easy.
+  exact Pos2Z.pos_is_nonneg.
 Qed.
 
 Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0.
 Proof.
- easy.
+  exact Pos2Z.neg_is_neg.
 Qed.
 
 Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n.