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/solvable/cyclic.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/solvable/cyclic.v')

diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v
index 8073449..9a1e451 100644
--- a/mathcomp/solvable/cyclic.v
+++ b/mathcomp/solvable/cyclic.v
@@ -316,7 +316,7 @@ Hypothesis dvd_y_x : #[y] %| #[x].
 Lemma eltmE i : eltm dvd_y_x (x ^+ i) = y ^+ i.
 Proof.
 apply/eqP; rewrite eq_expg_mod_order.
-have [x_le1 | x_gt1] := leqP #[x] 1. 
+have [x_le1 | x_gt1] := leqP #[x] 1.
   suffices: #[y] %| 1 by rewrite dvdn1 => /eqP->; rewrite !modn1.
   by rewrite (dvdn_trans dvd_y_x) // dvdn1 order_eq1 -cycle_eq1 trivg_card_le1.
 rewrite -(expg_znat i (cycle_id x)) invmE /=; last by rewrite /Zp x_gt1 inE.
@@ -536,7 +536,7 @@ Lemma metacyclicP A :
 Proof. exact: 'exists_and3P. Qed.
 
 Lemma metacyclic1 : metacyclic 1.
-Proof. 
+Proof.
 by apply/existsP; exists 1%G; rewrite normal1 trivg_quotient !cyclic1.
 Qed.
 
-- 
cgit v1.2.3