proposition: Lemma dH_wH u v : dH u (u + v) = wH v.
proof: Proof. by rewrite /dH opprD addrA subrr add0r wH_opp. 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