proposition: Lemma size_sol n f : size (sol n f) = n.
proof: Proof. rewrite /sol; case: sol_subproof => [sP | _]; last exact: size_nseq. by case/andP: (xchooseP sP) => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)