proposition: Lemma qpoly_mulA : associative (@qpoly_mul A h).
proof: Proof. have rPM := monic_mk_monic h; move=> p q r; apply: val_inj. by rewrite /= rmodp_mulml // rmodp_mulmr // mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun ssralg countalg finalg poly polydiv) mathcomp(perm fingroup matrix mxalgebra mxpoly vector countalg)