proposition: Lemma fsupp_pow r n : fsupp r -> fsupp (r ^^ n).
proof: Proof. ins; induction n; ins; eauto using fsupp_eqv, fsupp_union, fsupp_seq. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom