proposition: Lemma fcard_order_set n (a : {pred T}) : a \subset order_set n -> fclosed f a -> fcard f a * n = #|a|.
proof: Proof. move=> a_n cl_a; rewrite /n_comp_mem; set b := [predI froots f & a]. suff <-: #|preim (froot f) b| = #|b| * n. apply: eq_card => x; rewrite !inE (roots_root fconnect_sym). exact/esym/(closed_connect cl_a)/connect_root. have{cl_a a_n} (x): b x -> froot f x = x /\ order x = n. by case/andP=> /eqP-> /(subsetP a_n)/eqnP->. elim: {a b}#|b| {1 3 4}b (eqxx #|b|) => [|m IHm] b def_m f_b. by rewrite eq_card0 // => x; apply: (pred0P def_m). have [x b_x | b0] := pickP b; last by rewrite (eq_card0 b0) in def_m. have [r_x ox_n] := f_b x b_x; rewrite (cardD1 x) [x \in b]b_x eqSS in def_m. rewrite mulSn -{1}ox_n -(IHm _ def_m) => [|_ /andP[_ /f_b //]]. rewrite -(cardID (fconnect f x)); congr (_ + _); apply: eq_card => y. by apply: andb_idl => /= fxy; rewrite !inE -(rootP symf fxy) r_x. by congr (~~ _ && _); rewrite /= /in_mem /= symf -(root_connect symf) r_x. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)