proposition: Lemma monalgOver_oppr_closed : oppr_closed (monalgOver zmodS).
proof: Proof. move=> g Sg; apply/monalgOverP=> n; rewrite mcoeffN. by rewrite rpredN; apply/(monalgOverP zmodS). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap