From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 theories/Numbers/Integer/Abstract/ZDivEucl.v  | 2 +-
 theories/Numbers/Integer/Abstract/ZDivFloor.v | 2 +-
 theories/Numbers/Integer/Abstract/ZDivTrunc.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d0df8fb4a7..ab73ebfe1d 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -391,7 +391,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, 0<b -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index d5f3f4ada7..c8260e516f 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -436,7 +436,7 @@ rewrite <- (add_0_r (b*(a/b))) at 2.
 apply add_cancel_l.
 Qed.
 
-(** Some additionnal inequalities about div. *)
+(** Some additional inequalities about div. *)
 
 Theorem div_lt_upper_bound:
   forall a b q, 0<b -> a < b*q -> a/b < q.
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index de2e99ec3a..464fe354b8 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -404,7 +404,7 @@ Proof.
 intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto.
 Qed.
 
-(** Some additionnal inequalities about quot. *)
+(** Some additional inequalities about quot. *)
 
 Theorem quot_lt_upper_bound:
   forall a b q, 0<=a -> 0<b -> a < b*q -> a÷b < q.
-- 
cgit v1.2.3