summaryrefslogtreecommitdiff
path: root/theories/ZArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/BinInt.v23
1 files changed, 11 insertions, 12 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 2a615311..357d0b7e 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: BinInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: BinInt.v 13697 2010-12-09 18:48:04Z herbelin $ i*)
(***********************************************************)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
@@ -223,7 +223,6 @@ Qed.
(**********************************************************************)
-
(** ** Properties of opposite on binary integer numbers *)
Theorem Zopp_0 : Zopp Z0 = Z0.
@@ -270,21 +269,21 @@ Qed.
(**********************************************************************)
(** * Properties of the addition on integers *)
-(** ** zero is left neutral for addition *)
+(** ** Zero is left neutral for addition *)
Theorem Zplus_0_l : forall n:Z, Z0 + n = n.
Proof.
intro x; destruct x; reflexivity.
Qed.
-(** *** zero is right neutral for addition *)
+(** ** Zero is right neutral for addition *)
Theorem Zplus_0_r : forall n:Z, n + Z0 = n.
Proof.
intro x; destruct x; reflexivity.
Qed.
-(** ** addition is commutative *)
+(** ** Addition is commutative *)
Theorem Zplus_comm : forall n m:Z, n + m = m + n.
Proof.
@@ -296,7 +295,7 @@ Proof.
rewrite Pplus_comm; reflexivity.
Qed.
-(** ** opposite distributes over addition *)
+(** ** Opposite distributes over addition *)
Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
Proof.
@@ -310,7 +309,7 @@ Proof.
intro; unfold Zsucc; now rewrite Zopp_plus_distr.
Qed.
-(** ** opposite is inverse for addition *)
+(** ** Opposite is inverse for addition *)
Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
Proof.
@@ -327,7 +326,7 @@ Qed.
Hint Local Resolve Zplus_0_l Zplus_0_r.
-(** ** addition is associative *)
+(** ** Addition is associative *)
Lemma weak_assoc :
forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
@@ -495,7 +494,7 @@ Proof.
rewrite (Zplus_comm p n); trivial with arith.
Qed.
-(** ** addition simplifies *)
+(** ** Addition simplifies *)
Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
intros n m p H; cut (- n + (n + m) = - n + (n + p));
@@ -504,7 +503,7 @@ Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
| rewrite H; trivial with arith ].
Qed.
-(** ** addition and successor permutes *)
+(** ** Addition and successor permutes *)
Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
Proof.
@@ -575,7 +574,7 @@ Proof.
trivial with arith.
Qed.
-(** successor and predecessor are inverse functions *)
+(** ** Successor and predecessor are inverse functions *)
Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
Proof.
@@ -600,7 +599,7 @@ Proof.
Qed.
(*************************************************************************)
-(** ** Properties of the direct definition of successor and predecessor *)
+(** ** Properties of the direct definition of successor and predecessor *)
Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.
Proof.