From 37a49513f22a3f792a1ac3241962a7d17455f7e5 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 16 May 2020 09:02:13 +0900
Subject: A few more revisions

---
 mathcomp/ssreflect/fingraph.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

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

diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index b37ff2c..9fb79a2 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -747,9 +747,7 @@ by move=> x y xp yp; rewrite (orbitE fcycle_undup)// ?mem_rot ?mem_undup.
 Qed.
 
 Lemma eq_order_cycle : {in p &, forall x y, order y = order x}.
-Proof.
-by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup.
-Qed.
+Proof. by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup. Qed.
 
 Lemma iter_order_cycle : {in p &, forall x y, iter (order x) f y = y}.
 Proof.
-- 
cgit v1.2.3