proposition: Lemma mulmACA : interchange mul mul.
proof: Proof. by move=> x y z t; rewrite -!mulmA [_ y _]mulmCA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)