proposition: Lemma monalgOverS (S1 S2 : {pred G}) : {subset S1 <= S2} -> {subset monalgOver S1 <= monalgOver S2}.
proof: Proof. move=> le_S1S2 g /allP /= S1g; apply/allP => /= x Hx. exact/le_S1S2/S1g. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap