proposition: Lemma fsupp_cross (s s': A -> Prop) (F: set_finite s) : fsupp (s × s').
proof: Proof. unfolder in *; ins; desf; eexists; ins; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom