Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 11 insertions, 11 deletions

diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 59209370..eaa1bb2d 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Even.v 11512 2008-10-27 12:28:36Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
@@ -17,7 +17,7 @@ Open Local Scope nat_scope.
 Implicit Types m n : nat.
 
 
-(** * Definition of [even] and [odd], and basic facts *) 
+(** * Definition of [even] and [odd], and basic facts *)
 
 Inductive even : nat -> Prop :=
   | even_O : even 0
@@ -52,9 +52,9 @@ Qed.
 
 (** * Facts about [even] & [odd] wrt. [plus] *)
 
-Lemma even_plus_split : forall n m, 
+Lemma even_plus_split : forall n m,
   (even (n + m) -> even n /\ even m \/ odd n /\ odd m)
-with odd_plus_split : forall n m, 
+with odd_plus_split : forall n m,
   odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
 Proof.
 intros. clear even_plus_split. destruct n; simpl in *.
@@ -95,7 +95,7 @@ Proof.
   intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
   intro; destruct (not_even_and_odd n); auto.
 Qed.
- 
+
 Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
 Proof.
   intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
@@ -120,13 +120,13 @@ Proof.
   intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
   intro; destruct (not_even_and_odd m); auto.
 Qed.
- 
+
 Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
 Proof.
   intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
   intro; destruct (not_even_and_odd n); auto.
 Qed.
- 
+
 Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
 Proof.
   intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
@@ -203,7 +203,7 @@ Proof.
   intros n m; case (even_mult_aux n m); auto.
   intros H H0; case H0; auto.
 Qed.
- 
+
 Lemma even_mult_r : forall n m, even m -> even (n * m).
 Proof.
   intros n m; case (even_mult_aux n m); auto.
@@ -219,7 +219,7 @@ Proof.
   intros H'3; elim H'3; auto.
   intros H; case (not_even_and_odd n); auto.
 Qed.
- 
+
 Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.
 Proof.
   intros n m H' H'0.
@@ -228,13 +228,13 @@ Proof.
   intros H'3; elim H'3; auto.
   intros H; case (not_even_and_odd m); auto.
 Qed.
- 
+
 Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m).
 Proof.
   intros n m; case (even_mult_aux n m); intros H; case H; auto.
 Qed.
 Hint Resolve even_mult_l even_mult_r odd_mult: arith.
- 
+
 Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n.
 Proof.
   intros n m H'.