wip

cylinder.v

@@ -1386,10 +1386,20 @@ have sP: SAset_cast n (val s) \in [fset SAset_cast n s0 | s0 in S].
   apply/imfsetP; exists (val s) => //.
   exact/fsvalP.
 move=> /(_ [` sP])[] m [] xi [] xicont [] xisort SE.
-have: 
-
-
-
+have: val s \in [fset s
+        | s in [pred s0 in S |
+                 SAset_cast n s0 ==
+                 ((fsval (A:=[fset SAset_cast n s | s in S])).[sP])%fmap]].
+  by rewrite !inE/= eqxx andbT; apply/fsvalP.
+rewrite SE => /imfsetP[/=] t txi ->.
+apply/SAcast_connected.
+apply/(@SAconnected_partition_of_graphs_above _ _ (SAset_cast n (val s)) (val xi)).
+- exact/(IHn _ [` sP] SCD).
+- exact/xisort.
+- move=> /= i; rewrite size_tuple => im; move: (xicont (Ordinal im)).
+  by rewrite (tnth_nth 0).
+- by [].
+Qed.
 
 Theorem cylindrical_decomposition n (P : {fset {mpoly R[n]}}) :
   { S | isCD S /\ forall p : P, poly_adapted (val p) S}.
@@ -1669,8 +1679,7 @@ have size_gcd_const (s' : S') : {in P' s',
   rewrite -sgz_eq0 (res'_const s' p y x ys xs) ?sgz_eq0//.
   apply/leq_predn; rewrite -(S'size s' p x xs) -(size_deriv _ R0).
   exact/leq_gcdpr.
-have S'con (s' : S') : SAconnected (val s').
-  admit. (* s' connected *)
+have S'con (s' : S') : SAconnected (val s') by apply/SAconnected_CD_cell.
 have size_gcdpq_const (s' : S') : {in P' s' &,
   forall p q : {poly {mpoly R[n]}},
   {in \val s' &,