From fafd4dac5315e1d4e071b0044a50a16360b31964 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 23 Nov 2017 16:33:36 +0100
Subject: running semi-automated linting on the whole library

---
 mathcomp/ssreflect/div.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/div.v')

diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 723946d..4172430 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -200,7 +200,7 @@ rewrite leq_subLR addnA; apply: leq_trans (leq_divDl _ _ _).
 by rewrite -maxnE leq_div2r ?leq_maxr.
 Qed.
 
-Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p. 
+Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p.
 Proof.
 case: n p => [|n] [|p]; rewrite ?muln0 ?div0n //.
 rewrite {2}(divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //.
-- 
cgit v1.2.3