1 files changed, 37 insertions, 37 deletions
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index 9011cee3..1dec34e2 100644
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Div.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Div.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 (** Euclidean division *)
 
@@ -20,45 +20,45 @@ Require Compare_dec.
 Implicit Variables Type n,a,b,q,r:nat.
 
 Fixpoint inf_dec [n:nat] : nat->bool :=
-      [m:nat] Cases n m of
-                  O     _     => true
-              | (S n')  O     => false
-              | (S n') (S m') => (inf_dec n' m')
-             end.
+  [m:nat] Cases n m of
+            O     _     => true
+            | (S n')  O     => false
+            | (S n') (S m') => (inf_dec n' m')
+          end.
 
 Theorem div1 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
-Realizer Fix div1 {div1/2: nat->nat->diveucl :=
-  [b,a]Cases a of
-         O     => (O,O)
-       | (S n) =>
-           let (q,r) = (div1 b n) in
-             if (le_gt_dec b (S r)) then ((S q),O)
-	     else (q,(S r))
-       end}.
-Program_all.
-Rewrite e.
-Replace b with (S r).
-Simpl.
-Elim plus_n_O; Auto with arith.
-Apply le_antisym; Auto with arith.
-Elim plus_n_Sm; Auto with arith.
+  Realizer Fix div1 {div1/2: nat->nat->diveucl :=
+    [b,a]Cases a of
+           O     => (O,O)
+	   | (S n) =>
+             let (q,r) = (div1 b n) in
+               if (le_gt_dec b (S r)) then ((S q),O)
+		 else (q,(S r))
+	 end}.
+  Program_all.
+  Rewrite e.
+  Replace b with (S r).
+  Simpl.
+  Elim plus_n_O; Auto with arith.
+  Apply le_antisym; Auto with arith.
+  Elim plus_n_Sm; Auto with arith.
 Qed.
 
 Theorem div2 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
-Realizer Fix div1 {div1/2: nat->nat->diveucl :=
-  [b,a]Cases a of
-         O     => (O,O)
-       | (S n) =>
-           let (q,r) = (div1 b n) in
-             if (inf_dec b (S r)) :: :: { {(le b (S r))}+{(gt b (S r))} }
-             then ((S q),O)
-	     else (q,(S r))
-       end}.
-Program_all.
-Rewrite e.
-Replace b with (S r).
-Simpl.
-Elim plus_n_O; Auto with arith.
-Apply le_antisym; Auto with arith.
-Elim plus_n_Sm; Auto with arith.
+  Realizer Fix div1 {div1/2: nat->nat->diveucl :=
+    [b,a]Cases a of
+           O     => (O,O)
+	   | (S n) =>
+             let (q,r) = (div1 b n) in
+               if (inf_dec b (S r)) :: :: { {(le b (S r))}+{(gt b (S r))} }
+		 then ((S q),O)
+		 else (q,(S r))
+	 end}.
+  Program_all.
+  Rewrite e.
+  Replace b with (S r).
+  Simpl.
+  Elim plus_n_O; Auto with arith.
+  Apply le_antisym; Auto with arith.
+  Elim plus_n_Sm; Auto with arith.
 Qed.