From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 theories/ZArith/auxiliary.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'theories/ZArith/auxiliary.v')

diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index ffc3e70f..7af99ece 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,9 +7,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: auxiliary.v 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
 Require Import BinInt.
@@ -25,7 +26,7 @@ Open Local Scope Z_scope.
 Theorem Zne_left : forall n m:Z, Zne n m -> Zne (n + - m) 0.
 Proof.
   intros x y; unfold Zne in |- *; unfold not in |- *; intros H1 H2; apply H1;
-    apply Zplus_reg_l with (- y); rewrite Zplus_opp_l; 
+    apply Zplus_reg_l with (- y); rewrite Zplus_opp_l;
       rewrite Zplus_comm; trivial with arith.
 Qed.
 
@@ -97,7 +98,7 @@ Proof.
   intros x y z H1 H2 H3; apply Zle_trans with (m := y * x);
     [ apply Zmult_gt_0_le_0_compat; assumption
       | pattern (y * x) at 1 in |- *; rewrite <- Zplus_0_r;
-	apply Zplus_le_compat_l; apply Zlt_le_weak; apply Zgt_lt; 
+	apply Zplus_le_compat_l; apply Zlt_le_weak; apply Zgt_lt;
 	  assumption ].
 Qed.
 
-- 
cgit v1.2.3