proposition: Lemma dH_cat a b c d : size a = size c -> size b = size d -> dH (a ++ b) (c ++ d) = (dH a c + dH b d)%nat.
proof: Proof. move=> ac bd; by rewrite /dH /wH addb_seq_cat // /num_occ count_cat. 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