proposition: Lemma dH_count : forall n a b, size a = n -> dH (nseq n b) a = count (pred1 (negb b)) a.
proof: Proof. elim; first by case. move=> n IH [|[|] ta] [] // [H]; rewrite /dH in IH; by rewrite /= /dH /= IH. Qed.
imports: Reals mathcomp(all_ssreflect fingroup zmodp ssralg finalg perm matrix) mathcomp(poly mxalgebra mxpoly) mathcomp(Rstruct) ssr_ext ssralg_ext f2 num_occ natbin ssrR Reals_ext bigop_ext