Fix some typos.

3 files changed, 3 insertions, 3 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index d0d10891a..363b4fd03 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -279,7 +279,7 @@ Proof. intros; rewrite Z.div_exact; auto. Qed.
 Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a.
 Proof. intros. apply Z.mod_le; auto. Qed.
 
-(** Some additionnal inequalities about Z.div. *)
+(** Some additional inequalities about Z.div. *)
 
 Theorem Zdiv_lt_upper_bound:
   forall a b q, 0 < b -> a < q*b -> a/b < q.
diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v
index 8f661a9c8..c8627477b 100644
--- a/theories/ZArith/Zpow_alt.v
+++ b/theories/ZArith/Zpow_alt.v
@@ -11,7 +11,7 @@ Local Open Scope Z_scope.
 
 (** An alternative power function for Z *)
 
-(** This [Zpower_alt] is extensionnaly equal to [Z.pow],
+(** This [Zpower_alt] is extensionally equal to [Z.pow],
     but not convertible with it. The number of
     multiplications is logarithmic instead of linear, but
     these multiplications are bigger. Experimentally, it seems
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 3ef111898..6db92edb7 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -243,7 +243,7 @@ Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed.
 Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a.
 Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed.
 
-(** Some additionnal inequalities about Zdiv. *)
+(** Some additional inequalities about Zdiv. *)
 
 Theorem Zquot_le_upper_bound:
   forall a b q, 0 < b -> a <= q*b -> a÷b <= q.