Apply suggestion from @affeldt-aist

Author: affeldt-aist

theories/showcase/pnt.v

@@ -183,7 +183,7 @@ have: finset.trivIset (Parts i).
   rewrite -setI_eq0 -finset.subset0.
   apply/fintype.subsetP => x0.
   rewrite finset.in_setI !inE => /andP[] /mapP[]/= x1 x1x -> /mapP[]/= x2 x2y.
-  move=> /(congr1 val). rewrite !val_insubd. move: x1x x2y.
+  move=> /(congr1 val); rewrite !val_insubd; move: x1x x2y.
   rewrite !mem_iota !addnCB (Eigtpi x) // (Eigtpi y) // !addn0 !ltnS.
   have xiN (a : 'I_N.+1) (b : nat) : b <= a -> b <= N.
   by rewrite -![b <= _]ltnS; move=> /leq_trans; apply.