cleanup (80c lines)

cylinder.v

@@ -2305,11 +2305,15 @@ Qed.
 Definition lift_sample_cylindrical_decomposition n (P : {fset {mpoly R[n.+1]}})
     (s : 'rV[R]_n) :=
   [fset castmx (erefl, (@addn1 n)) (row_mx s (\row__ x)) | x in
-      let r := rootsR (\prod_(p : P | evalpmp s (muni (val p)) != 0) evalpmp s (muni (val p))) in
-          (head 0 r - 1) :: (last 0 r + 1) :: r ++ [seq (r`_i.+1 + r`_i) / 2 | i <- iota 0 (size r).-1]
+      let r := rootsR
+        (\prod_(p : P | evalpmp s (muni (val p)) != 0)
+            evalpmp s (muni (val p))) in
+      (head 0 r - 1) :: (last 0 r + 1) :: r
+      ++ [seq (r`_i.+1 + r`_i) / 2 | i <- iota 0 (size r).-1]
     ].
 
-Fixpoint sample_cylindrical_decomposition n : {fset {mpoly R[n]}} -> {fset 'rV[R]_n} :=
+Fixpoint sample_cylindrical_decomposition n :
+    {fset {mpoly R[n]}} -> {fset 'rV[R]_n} :=
   match n with
   | 0 => fun=> [fset \row__ 0]
   | S n => fun P =>
@@ -2428,16 +2432,6 @@ have ->: r = [seq (xi : {SAfun _ -> _}) (val x) ord0 ord0 | xi <- xi].
   move=> [/=] _ /imfsetP[/=] p + ->; rewrite inE => px0 _ py0.
   by apply/prodf_eq0; exists p => //; rewrite p0.
 set X := [fset _ | _ in _].
-(*case: (posnP (size xi)) => [/eqP|xi0].
-  rewrite size_eq0 => /eqP xi0.
-  have xP: (castmx (erefl, addn1 n) (row_mx (val x) (\row__ 1))) \in X.
-    apply/imfsetP; exists 1 => //=.
-    by rewrite 2!in_cons xi0/= !add0r eqxx orbT.
-  exists [` xP]; rewrite /= (inSAset_cast _ _ (esym (addn1 n))).
-  rewrite -[X in castmx (X, _)]/(esym (erefl 1%N)) castmxK inSAsetI inSAsetX.
-  rewrite row_mxKl xs inSAsetT !andbT.
-  move: ilt; rewrite xi0/= ltnS leqn0 => /eqP -> /=.
-   by rewrite big_nil inSAsetT. *)
 rewrite (nth_map 0%N); last by rewrite size_iota.
 rewrite nth_iota; last by [].
 case: (posnP i) => i0.