From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- theories/ZArith/auxiliary.v | 42 +----------------------------------------- 1 file changed, 1 insertion(+), 41 deletions(-) (limited to 'theories/ZArith/auxiliary.v') 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. -- cgit v1.2.3