proposition: Lemma fsupp_minus r r' : fsupp r -> fsupp (r \ r').
proof: Proof. unfolder; ins; desf. specialize (H y); desf; eauto; exists findom; ins; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom