Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 149 insertions, 149 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index eaf3f126a..e02f2817c 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -45,7 +45,7 @@ Definition Ndouble_plus_one x :=
 
 (** Operation x -> 2*x *)
 
-Definition Ndouble n := 
+Definition Ndouble n :=
   match n with
   | N0 => N0
   | Npos p => Npos (xO p)
@@ -130,12 +130,12 @@ Infix ">" := Ngt : N_scope.
 
 (** Min and max *)
 
-Definition Nmin (n n' : N) := match Ncompare n n' with 
+Definition Nmin (n n' : N) := match Ncompare n n' with
  | Lt | Eq => n
  | Gt => n'
  end.
 
-Definition Nmax (n n' : N) := match Ncompare n n' with 
+Definition Nmax (n n' : N) := match Ncompare n n' with
  | Lt | Eq => n'
  | Gt => n
  end.
@@ -149,7 +149,7 @@ Lemma N_ind_double :
    (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
 Proof.
   intros; elim a. trivial.
-  simple induction p. intros. 
+  simple induction p. intros.
   apply (H1 (Npos p0)); trivial.
   intros; apply (H0 (Npos p0)); trivial.
   intros; apply (H1 N0); assumption.
@@ -162,7 +162,7 @@ Lemma N_rec_double :
    (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
 Proof.
   intros; elim a. trivial.
-  simple induction p. intros. 
+  simple induction p. intros.
   apply (H1 (Npos p0)); trivial.
   intros; apply (H0 (Npos p0)); trivial.
   intros; apply (H1 N0); assumption.
@@ -354,7 +354,7 @@ destruct p; intros Hp H.
 contradiction Hp; reflexivity.
 destruct n; destruct m; reflexivity || (try discriminate H).
 injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity.
-Qed. 
+Qed.
 
 (** Properties of comparison *)
 
@@ -373,7 +373,7 @@ Qed.
 
 Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m.
 Proof.
-split; intros; 
+split; intros;
  [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ].
 Qed.
 
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index af281b73f..21ff55c19 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -32,15 +32,15 @@ Bind Scope positive_scope with positive.
 Arguments Scope xO [positive_scope].
 Arguments Scope xI [positive_scope].
 
-(** Postfix notation for positive numbers, allowing to mimic 
-    the position of bits in a big-endian representation. 
-    For instance, we can write 1~1~0 instead of (xO (xI xH)) 
+(** Postfix notation for positive numbers, allowing to mimic
+    the position of bits in a big-endian representation.
+    For instance, we can write 1~1~0 instead of (xO (xI xH))
     for the number 6 (which is 110 in binary notation).
 *)
 
-Notation "p ~ 1" := (xI p) 
+Notation "p ~ 1" := (xI p)
  (at level 7, left associativity, format "p '~' '1'") : positive_scope.
-Notation "p ~ 0" := (xO p) 
+Notation "p ~ 0" := (xO p)
  (at level 7, left associativity, format "p '~' '0'") : positive_scope.
 
 Open Local Scope positive_scope.
@@ -76,7 +76,7 @@ Fixpoint Pplus (x y:positive) : positive :=
     | 1, q~0 => q~1
     | 1, 1 => 1~0
   end
-  
+
 with Pplus_carry (x y:positive) : positive :=
   match x, y with
     | p~1, q~1 => (Pplus_carry p q)~1
@@ -178,7 +178,7 @@ Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask :=
     | 1, 1 => IsNul
     | 1, _ => IsNeg
   end
-  
+
 with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
   match x, y with
     | p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
@@ -255,13 +255,13 @@ Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
 
 
-Definition Pmin (p p' : positive) := match Pcompare p p' Eq with 
- | Lt | Eq => p 
+Definition Pmin (p p' : positive) := match Pcompare p p' Eq with
+ | Lt | Eq => p
  | Gt => p'
  end.
 
-Definition Pmax (p p' : positive) := match Pcompare p p' Eq with 
- | Lt | Eq => p' 
+Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
+ | Lt | Eq => p'
  | Gt => p
  end.
 
@@ -380,14 +380,14 @@ Theorem Pplus_comm : forall p q:positive, p + q = q + p.
 Proof.
   induction p; destruct q; simpl; f_equal; auto.
   rewrite 2 Pplus_carry_spec; f_equal; auto.
-Qed. 
+Qed.
 
 (** Permutation of [Pplus] and [Psucc] *)
 
 Theorem Pplus_succ_permute_r :
   forall p q:positive, p + Psucc q = Psucc (p + q).
 Proof.
-  induction p; destruct q; simpl; f_equal; 
+  induction p; destruct q; simpl; f_equal;
    auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto.
 Qed.
 
@@ -432,10 +432,10 @@ Qed.
 Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q.
 Proof.
   intros p q r; revert p q; induction r.
-  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; 
-    f_equal; auto using Pplus_carry_plus; 
+  intros [p|p| ] [q|q| ] H; simpl; destr_eq H;
+    f_equal; auto using Pplus_carry_plus;
     contradict H; auto using Pplus_carry_no_neutral.
-  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto; 
+  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto;
     contradict H; auto using Pplus_no_neutral.
   intros p q H; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption.
 Qed.
@@ -465,11 +465,11 @@ Qed.
 Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r.
 Proof.
   induction p.
-  intros [q|q| ] [r|r| ]; simpl; f_equal; auto; 
-    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, 
+  intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
+    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
      ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
   intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
-    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, 
+    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
      ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
   intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto.
 Qed.
@@ -493,7 +493,7 @@ Lemma Pplus_xO_double_minus_one :
   forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q.
 Proof.
   induction p as [p IHp| p IHp| ]; destruct q; simpl;
-  rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI, 
+  rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI,
     ?Pplus_xI_double_minus_one; try reflexivity.
   rewrite IHp; auto.
   rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity.
@@ -503,7 +503,7 @@ Qed.
 
 Lemma Pplus_diag : forall p:positive, p + p = p~0.
 Proof.
-  induction p as [p IHp| p IHp| ]; simpl; 
+  induction p as [p IHp| p IHp| ]; simpl;
    try rewrite ?Pplus_carry_spec, ?IHp; reflexivity.
 Qed.
 
@@ -534,10 +534,10 @@ Fixpoint peanoView p : PeanoView p :=
     | p~1 => peanoView_xI p (peanoView p)
   end.
 
-Definition PeanoView_iter (P:positive->Type) 
+Definition PeanoView_iter (P:positive->Type)
   (a:P 1) (f:forall p, P p -> P (Psucc p)) :=
   (fix iter p (q:PeanoView p) : P p :=
-    match q in PeanoView p return P p with 
+    match q in PeanoView p return P p with
       | PeanoOne => a
       | PeanoSucc _ q => f _ (iter _ q)
     end).
@@ -545,23 +545,23 @@ Definition PeanoView_iter (P:positive->Type)
 Require Import Eqdep_dec EqdepFacts.
 
 Theorem eq_dep_eq_positive :
-  forall (P:positive->Type) (p:positive) (x y:P p), 
+  forall (P:positive->Type) (p:positive) (x y:P p),
     eq_dep positive P p x p y -> x = y.
 Proof.
   apply eq_dep_eq_dec.
   decide equality.
 Qed.
 
-Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.  
+Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.
 Proof.
-  intros. 
+  intros.
   induction q as [ | p q IHq ].
   apply eq_dep_eq_positive.
   cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial.
   destruct p0; intros; discriminate.
   trivial.
   apply eq_dep_eq_positive.
-  cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. 
+  cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'.
   intro. destruct p; discriminate.
   intro. unfold p0 in H. apply Psucc_inj in H.
   generalize q'. rewrite H. intro.
@@ -570,12 +570,12 @@ Proof.
   trivial.
 Qed.
 
-Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)) 
+Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p))
   (p:positive) :=
   PeanoView_iter P a f p (peanoView p).
 
-Theorem Prect_succ : forall (P:positive->Type) (a:P 1) 
-  (f:forall p, P p -> P (Psucc p)) (p:positive), 
+Theorem Prect_succ : forall (P:positive->Type) (a:P 1)
+  (f:forall p, P p -> P (Psucc p)) (p:positive),
   Prect P a f (Psucc p) = f _ (Prect P a f p).
 Proof.
   intros.
@@ -584,7 +584,7 @@ Proof.
   trivial.
 Qed.
 
-Theorem Prect_base : forall (P:positive->Type) (a:P 1) 
+Theorem Prect_base : forall (P:positive->Type) (a:P 1)
   (f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a.
 Proof.
   trivial.
@@ -744,7 +744,7 @@ Qed.
 
 Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
 Proof.
-  induction p; intros [q| q| ] H; simpl in *; auto; 
+  induction p; intros [q| q| ] H; simpl in *; auto;
    try discriminate H; try (f_equal; auto; fail).
   destruct (Pcompare_not_Eq p q) as (H',_); elim H'; auto.
   destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto.
@@ -821,7 +821,7 @@ Lemma Pcompare_antisym :
   forall (p q:positive) (r:comparison),
     CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).
 Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto; 
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto;
    rewrite IHp; auto.
 Qed.
 
@@ -949,14 +949,14 @@ Qed.
 Theorem Pminus_mask_carry_spec :
   forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q).
 Proof.
-  induction p as [p IHp|p IHp| ]; destruct q; simpl; 
+  induction p as [p IHp|p IHp| ]; destruct q; simpl;
    try reflexivity; try rewrite IHp;
    destruct (Pminus_mask p q) as [|[r|r| ]|] || destruct p; auto.
 Qed.
 
 Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q).
 Proof.
-  intros p q; unfold Pminus; 
+  intros p q; unfold Pminus;
   rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
   destruct (Pminus_mask p q) as [|[r|r| ]|]; auto.
 Qed.
@@ -995,11 +995,11 @@ Proof.
   induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
 Qed.
 
-Lemma Pminus_mask_IsNeg : forall p q:positive, 
+Lemma Pminus_mask_IsNeg : forall p q:positive,
  Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
 Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; 
-   try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H; 
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto;
+   try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H;
    specialize IHp with q.
   destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
   destruct (Pminus_mask p q); simpl; auto; try discriminate.
@@ -1028,9 +1028,9 @@ Lemma Pminus_mask_Gt :
       Pminus_mask p q = IsPos h /\
       q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).
 Proof.
-  induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; 
+  induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *;
    try discriminate H.
-  (* p~1, q~1 *) 
+  (* p~1, q~1 *)
   destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
   repeat split; auto; right.
   destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
@@ -1091,10 +1091,10 @@ Qed.
 
 (** Number of digits in a number *)
 
-Fixpoint Psize (p:positive) : nat := 
-  match p with 
+Fixpoint Psize (p:positive) : nat :=
+  match p with
     | 1 => S O
-    | p~1 => S (Psize p) 
+    | p~1 => S (Psize p)
     | p~0 => S (Psize p)
   end.
 
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index e9bc4b266..ef381c7f2 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -45,7 +45,7 @@ Proof.
 Qed.
 
 Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true.
-Proof. 
+Proof.
 intros; rewrite <- (Pcompare_Eq_eq _ _ H).
 apply Peqb_correct.
 Qed.
@@ -69,7 +69,7 @@ Proof.
 Qed.
 
 Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true.
-Proof. 
+Proof.
 intros; rewrite <- (Ncompare_Eq_eq _ _ H).
 apply Neqb_correct.
 Qed.
@@ -107,7 +107,7 @@ Lemma Nodd_not_double :
    Nodd a -> forall a0, Neqb (Ndouble a0) a = false.
 Proof.
   intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H. 
+  rewrite <- (Neqb_complete _ _ H0) in H.
   unfold Nodd in H.
   rewrite (Ndouble_bit0 a0) in H. discriminate H.
   trivial.
@@ -128,7 +128,7 @@ Lemma Neven_not_double_plus_one :
    Neven a -> forall a0, Neqb (Ndouble_plus_one a0) a = false.
 Proof.
   intros. elim (sumbool_of_bool (Neqb (Ndouble_plus_one a0) a)). intro H0.
-  rewrite <- (Neqb_complete _ _ H0) in H. 
+  rewrite <- (Neqb_complete _ _ H0) in H.
   unfold Neven in H.
   rewrite (Ndouble_plus_one_bit0 a0) in H.
   discriminate H.
@@ -391,8 +391,8 @@ Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b.
 Proof.
  unfold Nmin, Nmin', Nleb; intros.
  rewrite nat_of_Ncompare.
- generalize (leb_compare (nat_of_N a) (nat_of_N b)); 
- destruct (nat_compare (nat_of_N a) (nat_of_N b)); 
+ generalize (leb_compare (nat_of_N a) (nat_of_N b));
+ destruct (nat_compare (nat_of_N a) (nat_of_N b));
  destruct (leb (nat_of_N a) (nat_of_N b)); intuition.
  lapply H1; intros; discriminate.
  lapply H1; intros; discriminate.
@@ -421,7 +421,7 @@ Qed.
 Lemma Nmin_le_3 :
  forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true.
 Proof.
-  intros; rewrite Nmin_Nmin' in *. 
+  intros; rewrite Nmin_Nmin' in *.
   unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
   assumption.
   intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption.
@@ -430,7 +430,7 @@ Qed.
 Lemma Nmin_le_4 :
  forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true.
 Proof.
-  intros; rewrite Nmin_Nmin' in *. 
+  intros; rewrite Nmin_Nmin' in *.
   unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
   apply Nleb_trans with (b := b); assumption.
   intro H0. rewrite H0 in H. assumption.
@@ -447,7 +447,7 @@ Qed.
 Lemma Nmin_lt_3 :
  forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false.
 Proof.
-  intros; rewrite Nmin_Nmin' in *. 
+  intros; rewrite Nmin_Nmin' in *.
   unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
   assumption.
   intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption.
@@ -456,7 +456,7 @@ Qed.
 Lemma Nmin_lt_4 :
  forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false.
 Proof.
-  intros; rewrite Nmin_Nmin' in *. 
+  intros; rewrite Nmin_Nmin' in *.
   unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
   apply Nltb_leb_trans with (b := b); assumption.
   intro H0. rewrite H0 in H. assumption.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index ea5f02bba..b1f2668e6 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -27,7 +27,7 @@ Fixpoint Pxor (p1 p2:positive) {struct p1} : N :=
   | xO p1, xI p2 => Ndouble_plus_one (Pxor p1 p2)
   | xI p1, xH => Npos (xO p1)
   | xI p1, xO p2 => Ndouble_plus_one (Pxor p1 p2)
-  | xI p1, xI p2 => Ndouble (Pxor p1 p2) 
+  | xI p1, xI p2 => Ndouble (Pxor p1 p2)
   end.
 
 Definition Nxor (n n':N) :=
@@ -65,7 +65,7 @@ Proof.
   simpl. rewrite IHp; reflexivity.
 Qed.
 
-(** Checking whether a particular bit is set on not *) 
+(** Checking whether a particular bit is set on not *)
 
 Fixpoint Pbit (p:positive) : nat -> bool :=
   match p with
@@ -134,13 +134,13 @@ Qed.
 
 (** End of auxilliary results *)
 
-(** This part is aimed at proving that if two numbers produce 
+(** This part is aimed at proving that if two numbers produce
   the same stream of bits, then they are equal. *)
 
 Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a.
 Proof.
   destruct a. trivial.
-  induction p as [p IHp| p IHp| ]; intro H. 
+  induction p as [p IHp| p IHp| ]; intro H.
   absurd (N0 = Npos p). discriminate.
   exact (IHp (fun n => H (S n))).
   absurd (N0 = Npos p). discriminate.
@@ -196,7 +196,7 @@ Proof.
   assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
   inversion H1. reflexivity.
   assumption.
-  intros. apply Nbit_faithful_3. intros. 
+  intros. apply Nbit_faithful_3. intros.
   assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
   inversion H1. reflexivity.
   assumption.
@@ -257,7 +257,7 @@ Proof.
   generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H.
   unfold xorf in *.
   destruct a as [|p]. simpl Nbit; rewrite false_xorb. reflexivity.
-  destruct a' as [|p0]. 
+  destruct a' as [|p0].
   simpl Nbit; rewrite xorb_false. reflexivity.
   destruct p. destruct p0; simpl Nbit in *.
   rewrite <- H; simpl; case (Pxor p p0); trivial.
@@ -273,13 +273,13 @@ Qed.
 Lemma Nxor_semantics :
  forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')).
 Proof.
-  unfold eqf. intros; generalize a, a'. induction n. 
+  unfold eqf. intros; generalize a, a'. induction n.
   apply Nxor_sem_5. apply Nxor_sem_6; assumption.
 Qed.
 
-(** Consequences: 
+(** Consequences:
        - only equal numbers lead to a null xor
-       - xor is associative 
+       - xor is associative
 *)
 
 Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'.
@@ -306,7 +306,7 @@ Proof.
   apply eqf_sym, Nxor_semantics.
 Qed.
 
-(** Checking whether a number is odd, i.e. 
+(** Checking whether a number is odd, i.e.
    if its lower bit is set. *)
 
 Definition Nbit0 (n:N) :=
@@ -380,8 +380,8 @@ Lemma Nneg_bit0 :
  forall a a':N,
    Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a').
 Proof.
-  intros. 
-  rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. 
+  intros.
+  rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false.
   reflexivity.
 Qed.
 
@@ -402,7 +402,7 @@ Lemma Nsame_bit0 :
  forall (a a':N) (p:positive),
    Nxor a a' = Npos (xO p) -> Nbit0 a = Nbit0 a'.
 Proof.
-  intros. rewrite <- (xorb_false (Nbit0 a)). 
+  intros. rewrite <- (xorb_false (Nbit0 a)).
   assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity.
   rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity.
 Qed.
@@ -430,7 +430,7 @@ Proof.
   assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
   simpl. rewrite H, H0. reflexivity.
-  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). 
+  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
 Qed.
 
@@ -443,7 +443,7 @@ Proof.
   assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
   simpl. rewrite H, H0. reflexivity.
-  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). 
+  assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
   rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
 Qed.
 
@@ -534,7 +534,7 @@ Proof.
         rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H.
           rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0).
 Qed.
- 
+
 Lemma Nless_total :
  forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
 Proof.
@@ -558,7 +558,7 @@ Qed.
 
 (** Number of digits in a number *)
 
-Definition Nsize (n:N) : nat := match n with 
+Definition Nsize (n:N) : nat := match n with
   | N0 => 0%nat
   | Npos p => Psize p
  end.
@@ -566,35 +566,35 @@ Definition Nsize (n:N) : nat := match n with
 
 (** conversions between N and bit vectors. *)
 
-Fixpoint P2Bv (p:positive) : Bvector (Psize p) := 
- match p return Bvector (Psize p) with 
+Fixpoint P2Bv (p:positive) : Bvector (Psize p) :=
+ match p return Bvector (Psize p) with
    | xH => Bvect_true 1%nat
    | xO p => Bcons false (Psize p) (P2Bv p)
    | xI p => Bcons true (Psize p) (P2Bv p)
  end.
 
 Definition N2Bv (n:N) : Bvector (Nsize n) :=
-  match n as n0 return Bvector (Nsize n0) with 
+  match n as n0 return Bvector (Nsize n0) with
     | N0 => Bnil
     | Npos p => P2Bv p
   end.
 
-Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N := 
-  match bv with 
+Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N :=
+  match bv with
     | Vnil => N0
     | Vcons false n bv => Ndouble (Bv2N n bv)
-    | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) 
+    | Vcons true n bv => Ndouble_plus_one (Bv2N n bv)
   end.
 
 Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
-Proof. 
+Proof.
 destruct n.
 simpl; auto.
 induction p; simpl in *; auto; rewrite IHp; simpl; auto.
 Qed.
 
-(** The opposite composition is not so simple: if the considered 
-  bit vector has some zeros on its right, they will disappear during 
+(** The opposite composition is not so simple: if the considered
+  bit vector has some zeros on its right, they will disappear during
   the return [Bv2N] translation: *)
 
 Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n.
@@ -603,16 +603,16 @@ induction n; intros.
 rewrite (V0_eq _ bv); simpl; auto.
 rewrite (VSn_eq _ _ bv); simpl.
 specialize IHn with (Vtail _ _ bv).
-destruct (Vhead _ _ bv); 
- destruct (Bv2N n (Vtail bool n bv)); 
+destruct (Vhead _ _ bv);
+ destruct (Bv2N n (Vtail bool n bv));
   simpl; auto with arith.
 Qed.
 
 (** In the previous lemma, we can only replace the inequality by
   an equality whenever the highest bit is non-null. *)
 
-Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), 
-  Bsign _ bv = true <-> 
+Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
+  Bsign _ bv = true <->
   Nsize (Bv2N _ bv) = (S n).
 Proof.
 induction n; intro.
@@ -621,18 +621,18 @@ rewrite (V0_eq _ (Vtail _ _ bv)); simpl.
 destruct (Vhead _ _ bv); simpl; intuition; try discriminate.
 rewrite (VSn_eq _ _ bv); simpl.
 generalize (IHn (Vtail _ _ bv)); clear IHn.
-destruct (Vhead _ _ bv); 
- destruct (Bv2N (S n) (Vtail bool (S n) bv)); 
+destruct (Vhead _ _ bv);
+ destruct (Bv2N (S n) (Vtail bool (S n) bv));
   simpl; intuition; try discriminate.
 Qed.
 
-(** To state nonetheless a second result about composition of 
- conversions, we define a conversion on a given number of bits : *) 
+(** To state nonetheless a second result about composition of
+ conversions, we define a conversion on a given number of bits : *)
 
-Fixpoint N2Bv_gen (n:nat)(a:N) { struct n } : Bvector n := 
- match n return Bvector n with 
+Fixpoint N2Bv_gen (n:nat)(a:N) { struct n } : Bvector n :=
+ match n return Bvector n with
    | 0 => Bnil
-   | S n => match a with 
+   | S n => match a with
        | N0 => Bvect_false (S n)
        | Npos xH => Bcons true _ (Bvect_false n)
        | Npos (xO p) => Bcons false _ (N2Bv_gen n (Npos p))
@@ -649,10 +649,10 @@ auto.
 induction p; simpl; intros; auto; congruence.
 Qed.
 
-(** In fact, if [k] is large enough, [N2Bv_gen k a] contains all digits of 
+(** In fact, if [k] is large enough, [N2Bv_gen k a] contains all digits of
    [a] plus some zeros. *)
 
-Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), 
+Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat),
  N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k).
 Proof.
 destruct a; simpl.
@@ -662,7 +662,7 @@ Qed.
 
 (** Here comes now the second composition result. *)
 
-Lemma N2Bv_Bv2N : forall n (bv:Bvector n), 
+Lemma N2Bv_Bv2N : forall n (bv:Bvector n),
    N2Bv_gen n (Bv2N n bv) = bv.
 Proof.
 induction n; intros.
@@ -670,21 +670,21 @@ rewrite (V0_eq _ bv); simpl; auto.
 rewrite (VSn_eq _ _ bv); simpl.
 generalize (IHn (Vtail _ _ bv)); clear IHn.
 unfold Bcons.
-destruct (Bv2N _ (Vtail _ _ bv)); 
- destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial; 
+destruct (Bv2N _ (Vtail _ _ bv));
+ destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial;
   induction n; simpl; auto.
 Qed.
 
 (** accessing some precise bits. *)
 
-Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), 
+Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
   Nbit0 (Bv2N _ bv) = Blow _ bv.
 Proof.
 intros.
 unfold Blow.
 rewrite (VSn_eq _ _ bv) at 1.
 simpl.
-destruct (Bv2N n (Vtail bool n bv)); simpl; 
+destruct (Bv2N n (Vtail bool n bv)); simpl;
  destruct (Vhead bool n bv); auto.
 Qed.
 
@@ -699,7 +699,7 @@ Proof.
  apply (IHbv p); auto with arith.
 Defined.
 
-Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), 
+Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
   Bnth _ bv p H = Nbit (Bv2N _ bv) p.
 Proof.
 induction bv; intros.
@@ -726,7 +726,7 @@ Qed.
 
 (** Xor is the same in the two worlds. *)
 
-Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), 
+Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
   Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').
 Proof.
 induction n.
@@ -735,7 +735,7 @@ rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
 intros.
 rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
 rewrite IHn.
-destruct (Vhead bool n bv); destruct (Vhead bool n bv'); 
+destruct (Vhead bool n bv); destruct (Vhead bool n bv');
  destruct (Bv2N n (Vtail bool n bv)); destruct (Bv2N n (Vtail bool n bv')); simpl; auto.
 Qed.
 
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v
index 678d37c1e..92559ff67 100644
--- a/theories/NArith/Ndist.v
+++ b/theories/NArith/Ndist.v
@@ -34,7 +34,7 @@ Definition Nplength (a:N) :=
 
 Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0.
 Proof.
-  simple induction a; trivial. 
+  simple induction a; trivial.
   unfold Nplength in |- *; intros; discriminate H.
 Qed.
 
@@ -42,7 +42,7 @@ Lemma Nplength_zeros :
  forall (a:N) (n:nat),
    Nplength a = ni n -> forall k:nat, k < n -> Nbit a k = false.
 Proof.
-  simple induction a; trivial. 
+  simple induction a; trivial.
   simple induction p. simple induction n. intros. inversion H1.
   simple induction k. simpl in H1. discriminate H1.
   intros. simpl in H1. discriminate H1.
@@ -116,11 +116,11 @@ Qed.
 Lemma ni_min_assoc :
  forall d d' d'':natinf, ni_min (ni_min d d') d'' = ni_min d (ni_min d' d'').
 Proof.
-  simple induction d; trivial. simple induction d'; trivial. 
+  simple induction d; trivial. simple induction d'; trivial.
   simple induction d''; trivial.
   unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)).
   intro. rewrite H. reflexivity.
-  generalize n0 n1. elim n; trivial. 
+  generalize n0 n1. elim n; trivial.
   simple induction n3; trivial. simple induction n5; trivial.
   intros. simpl in |- *. auto.
 Qed.
@@ -250,10 +250,10 @@ Proof.
 Qed.
 
 
-(** We define an ultrametric distance between [N] numbers: 
-    $d(a,a')=1/2^pd(a,a')$, 
-    where $pd(a,a')$ is the number of identical bits at the beginning 
-    of $a$ and $a'$ (infinity if $a=a'$).  
+(** We define an ultrametric distance between [N] numbers:
+    $d(a,a')=1/2^pd(a,a')$,
+    where $pd(a,a')$ is the number of identical bits at the beginning
+    of $a$ and $a'$ (infinity if $a=a'$).
     Instead of working with $d$, we work with $pd$, namely
     [Npdist]: *)
 
@@ -286,7 +286,7 @@ Qed.
   This follows from the fact that $a ~Ra~|a| = 1/2^{\texttt{Nplength}}(a))$
   is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$,
   or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that
-  min $(\texttt{Nplength}(a), \texttt{Nplength}(b)) \leq 
+  min $(\texttt{Nplength}(a), \texttt{Nplength}(b)) \leq
   \texttt{Nplength} (a~\texttt{xor}~ b)$
   (lemma [Nplength_ultra]).
 *)
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 36a1f1d8f..0016d035f 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -39,7 +39,7 @@ Definition N_of_nat (n:nat) :=
 Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a.
 Proof.
   destruct a as [| p]. reflexivity.
-  simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. 
+  simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *.
   rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H.
   rewrite nat_of_P_inj with (1 := H). reflexivity.
 Qed.
@@ -66,14 +66,14 @@ Proof.
   apply N_of_nat_of_N.
 Qed.
 
-Lemma nat_of_Ndouble_plus_one : 
+Lemma nat_of_Ndouble_plus_one :
   forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).
 Proof.
   destruct a; simpl nat_of_N; auto.
   apply nat_of_P_xI.
 Qed.
 
-Lemma N_of_double_plus_one : 
+Lemma N_of_double_plus_one :
   forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).
 Proof.
   intros.
@@ -97,14 +97,14 @@ Proof.
   apply N_of_nat_of_N.
 Qed.
 
-Lemma nat_of_Nplus : 
+Lemma nat_of_Nplus :
   forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a').
 Proof.
   destruct a; destruct a'; simpl; auto.
   apply nat_of_P_plus_morphism.
 Qed.
 
-Lemma N_of_plus : 
+Lemma N_of_plus :
   forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').
 Proof.
   intros.
@@ -138,14 +138,14 @@ Proof.
   apply N_of_nat_of_N.
 Qed.
 
-Lemma nat_of_Nmult : 
+Lemma nat_of_Nmult :
   forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
 Proof.
   destruct a; destruct a'; simpl; auto.
   apply nat_of_P_mult_morphism.
 Qed.
 
-Lemma N_of_mult : 
+Lemma N_of_mult :
   forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').
 Proof.
   intros.
@@ -155,7 +155,7 @@ Proof.
   apply N_of_nat_of_N.
 Qed.
 
-Lemma nat_of_Ndiv2 : 
+Lemma nat_of_Ndiv2 :
   forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N a).
 Proof.
   destruct a; simpl in *; auto.
@@ -164,9 +164,9 @@ Proof.
   rewrite div2_double_plus_one; auto.
   rewrite nat_of_P_xO.
   rewrite div2_double; auto.
-Qed.  
+Qed.
 
-Lemma N_of_div2 : 
+Lemma N_of_div2 :
   forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).
 Proof.
   intros.
@@ -175,7 +175,7 @@ Proof.
   apply N_of_nat_of_N.
 Qed.
 
-Lemma nat_of_Ncompare : 
+Lemma nat_of_Ncompare :
  forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a').
 Proof.
   destruct a; destruct a'; simpl.
@@ -187,7 +187,7 @@ Proof.
   apply nat_of_P_compare_morphism.
 Qed.
 
-Lemma N_of_nat_compare : 
+Lemma N_of_nat_compare :
  forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').
 Proof.
   intros.
@@ -321,17 +321,17 @@ Qed.
 Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n.
 Proof.
  destruct n; simpl; auto.
-Qed. 
+Qed.
 
 Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.
 Proof.
  destruct p; simpl; auto.
-Qed. 
+Qed.
 
 Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.
 Proof.
  destruct z; simpl; auto.
-Qed. 
+Qed.
 
 Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z.
 Proof.
@@ -348,22 +348,22 @@ Proof.
  destruct n; destruct m; auto.
 Qed.
 
-Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). 
+Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m).
 Proof.
  intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus.
 Qed.
 
-Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). 
+Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n).
 Proof.
  intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S.
 Qed.
 
-Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). 
+Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m).
 Proof.
  intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min.
 Qed.
 
-Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). 
+Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m).
 Proof.
  intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max.
 Qed.
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v
index bf42c5e99..f989e01d0 100644
--- a/theories/NArith/Pnat.v
+++ b/theories/NArith/Pnat.v
@@ -11,7 +11,7 @@
 Require Import BinPos.
 
 (**********************************************************************)
-(** Properties of the injection from binary positive numbers to Peano 
+(** Properties of the injection from binary positive numbers to Peano
     natural numbers *)
 
 (** Original development by Pierre Crégut, CNET, Lannion, France *)
@@ -50,7 +50,7 @@ Proof.
 intro x; induction x as [p IHp| p IHp| ]; intro y;
  [ destruct y as [p0| p0| ]
  | destruct y as [p0| p0| ]
- | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; 
+ | destruct y as [p| p| ] ]; simpl in |- *; auto with arith;
  intro m;
  [ rewrite IHp; rewrite plus_assoc; trivial with arith
  | rewrite IHp; rewrite plus_assoc; trivial with arith
@@ -75,11 +75,11 @@ intro x; induction x as [p IHp| p IHp| ]; intro y;
  | destruct y as [p| p| ] ]; simpl in |- *; auto with arith;
  [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp;
     rewrite plus_assoc_reverse; rewrite plus_assoc_reverse;
-    rewrite (plus_permute m (Pmult_nat p (m + m))); 
+    rewrite (plus_permute m (Pmult_nat p (m + m)));
     trivial with arith
  | intros m; rewrite IHp; apply plus_assoc
  | intros m; rewrite Pmult_nat_succ_morphism;
-    rewrite (plus_comm (m + Pmult_nat p (m + m))); 
+    rewrite (plus_comm (m + Pmult_nat p (m + m)));
     apply plus_assoc_reverse
  | intros m; rewrite IHp; apply plus_permute
  | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].
@@ -110,7 +110,7 @@ Proof.
 intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism;
  trivial.
 Qed.
- 
+
 (** [nat_of_P] is a morphism for multiplication *)
 
 Theorem nat_of_P_mult_morphism :
@@ -133,11 +133,11 @@ Proof.
 intro y; induction y as [p H| p H| ];
  [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *;
     simpl in |- *; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; 
+    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1;
     rewrite H1; auto with arith
  | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *;
     simpl in |- *; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; 
+    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2;
     rewrite H2; auto with arith
  | exists 0; auto with arith ].
 Qed.
@@ -182,7 +182,7 @@ intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ];
     apply ZL7; apply H; assumption
  | simpl in |- *; discriminate H2
  | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6;
-    elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; 
+    elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *;
     apply lt_O_Sn
  | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q);
     intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;
@@ -314,7 +314,7 @@ Proof.
 Qed.
 
 (**********************************************************************)
-(** Properties of the shifted injection from Peano natural numbers to 
+(** Properties of the shifted injection from Peano natural numbers to
     binary positive numbers *)
 
 (** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *)
@@ -366,7 +366,7 @@ intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto.
 Qed.
 
 (**********************************************************************)
-(** Extra properties of the injection from binary positive numbers to Peano 
+(** Extra properties of the injection from binary positive numbers to Peano
     natural numbers *)
 
 (** [nat_of_P] is a morphism for subtraction on positive numbers *)
@@ -384,14 +384,14 @@ Qed.
 Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p.
 Proof.
 intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1;
- rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; 
+ rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S;
  apply le_minus.
 Qed.
 
 Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q).
 Proof.
 intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q);
- intros k H; rewrite H; rewrite plus_comm; simpl in |- *; 
+ intros k H; rewrite H; rewrite plus_comm; simpl in |- *;
  apply le_n_S; apply le_plus_r.
 Qed.
 
@@ -410,7 +410,7 @@ intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
        [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);
           rewrite plus_assoc; rewrite le_plus_minus_r;
           [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l;
-             apply nat_of_P_lt_Lt_compare_morphism; 
+             apply nat_of_P_lt_Lt_compare_morphism;
              assumption
           | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
              apply ZC1; assumption ]
@@ -454,7 +454,7 @@ intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism;
     [ do 2 rewrite nat_of_P_mult_morphism;
        do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r
     | apply nat_of_P_gt_Gt_compare_complement_morphism;
-       do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; 
+       do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *;
        elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l;
        exact (nat_of_P_gt_Gt_compare_morphism y z H) ]
  | assumption ].