proposition: Lemma fsupp_union_iff r1 r2 : fsupp (r1 ∪ r2) <-> fsupp r1 /\ fsupp r2.
proof: Proof. unfolder in *; intuition; repeat match goal with [ H : _, y : A |- _ ] => specialize (H y) end; desf; first [exists (findom ++ findom0) | exists findom]; ins; desf; eauto using in_or_app. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom