Arithemtic: more concerning compare, eqb, leb, ltb

 Start of a uniform treatment of compare, eqb, leb, ltb:
 - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
 - Some generic properties are derived in OrdersFacts.BoolOrderFacts

 In BinPos, more work about sub_mask with nice implications
 on compare (e.g. simplier proof of lt_trans).

 In BinNat/BinPos, for uniformity, compare_antisym is now
 (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.

 In BigN / BigZ, eq_bool is now eqb

 In BinIntDef, gtb and geb are kept for the moment, but
 a comment advise to rather use ltb and leb. Z.div now uses
 Z.ltb and Z.leb.

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 2fdfad5dd..bc3d73484 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -173,7 +173,7 @@ Qed.
 Lemma inj_sub_max n m : Z.of_N (n-m) = Z.max 0 (Z.of_N n - Z.of_N m).
 Proof.
  destruct n as [|n], m as [|m]; simpl; trivial.
- rewrite Z.pos_sub_spec, <- Pos.sub_mask_compare. unfold Pos.sub.
+ rewrite Z.pos_sub_spec, Pos.compare_sub_mask. unfold Pos.sub.
  now destruct (Pos.sub_mask n m).
 Qed.
 
@@ -181,7 +181,7 @@ Lemma inj_sub n m : (m<=n)%N -> Z.of_N (n-m) = Z.of_N n - Z.of_N m.
 Proof.
  intros H. rewrite inj_sub_max.
  unfold N.le in H.
- rewrite <- N.compare_antisym, <- inj_compare, Z.compare_sub in H.
+ rewrite N.compare_antisym, <- inj_compare, Z.compare_sub in H.
  destruct (Z.of_N n - Z.of_N m); trivial; now destruct H.
 Qed.
 
@@ -275,7 +275,7 @@ Lemma inj_sub n m : 0<=m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N.
 Proof.
  destruct n as [|n|n], m as [|m|m]; trivial; try (now destruct 1).
  intros _. simpl.
- rewrite Z.pos_sub_spec, <- Pos.sub_mask_compare. unfold Pos.sub.
+ rewrite Z.pos_sub_spec, Pos.compare_sub_mask. unfold Pos.sub.
  now destruct (Pos.sub_mask n m).
 Qed.