diff options
| author | Kazuhiko Sakaguchi | 2020-05-16 09:02:13 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-05-16 09:30:39 +0900 |
| commit | 37a49513f22a3f792a1ac3241962a7d17455f7e5 (patch) | |
| tree | 3f3f5a094547ae1166a21cb7c5350c7e5a87404a /mathcomp/ssreflect/fingraph.v | |
| parent | 35bd8708dacfb508f896d957d7b1189ca7decb3e (diff) | |
A few more revisions
Diffstat (limited to 'mathcomp/ssreflect/fingraph.v')
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 4 |
1 files changed, 1 insertions, 3 deletions
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. |