summaryrefslogtreecommitdiff
path: root/theories/ZArith/auxiliary.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /theories/ZArith/auxiliary.v
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/ZArith/auxiliary.v')
-rw-r--r--theories/ZArith/auxiliary.v42
1 files changed, 1 insertions, 41 deletions
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 726fb45a..ffc3e70f 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auxiliary.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: auxiliary.v 11739 2009-01-02 19:33:19Z herbelin $ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
@@ -91,46 +91,6 @@ Proof.
rewrite Zplus_opp_r; trivial.
Qed.
-(**********************************************************************)
-(** * Factorization lemmas *)
-
-Theorem Zred_factor0 : forall n:Z, n = n * 1.
- intro x; rewrite (Zmult_1_r x); reflexivity.
-Qed.
-
-Theorem Zred_factor1 : forall n:Z, n + n = n * 2.
-Proof.
- exact Zplus_diag_eq_mult_2.
-Qed.
-
-Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m).
-Proof.
- intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x);
- rewrite <- Zmult_plus_distr_r; trivial with arith.
-Qed.
-
-Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m).
-Proof.
- intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x);
- rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm;
- trivial with arith.
-Qed.
-
-Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p).
-Proof.
- intros x y z; symmetry in |- *; apply Zmult_plus_distr_r.
-Qed.
-
-Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m.
-Proof.
- intros x y; rewrite <- Zmult_0_r_reverse; auto with arith.
-Qed.
-
-Theorem Zred_factor6 : forall n:Z, n = n + 0.
-Proof.
- intro; rewrite Zplus_0_r; trivial with arith.
-Qed.
-
Theorem Zle_mult_approx :
forall n m p:Z, n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p.
Proof.