proposition: Lemma dH_sym n a b : size a = n -> size b = n -> dH a b = dH b a.
proof: Proof. move=> Ha Hb. by rewrite /dH (@addb_seq_com n). 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