proposition: Lemma fsupp_restr r (FS: fsupp r) cond : fsupp (restr_rel cond r).
proof: Proof. firstorder. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom