diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 23 |
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. |