proposition: Lemma solP n f : reflect (exists2 s, size s = n & holds s f) (sat (sol n f) f).
proof: Proof. rewrite /sol; case: sol_subproof => [sP | sPn]. case/andP: (xchooseP sP) => _ ->; left. by case: sP => s; case/andP; move/eqP=> <-; move/satP; exists s. apply: (iffP (satP _ _)); first by exists (nseq n 0); rewrite ?size_nseq. by case=> s sz_s; move/satP=> f_s; case: sPn; exists s; rewrite sz_s eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)