proposition: Lemma fsupp_seq r1 r2 (FS1: fsupp r1) (FS2: fsupp r2) : fsupp (r1 ⨾ r2).
proof: Proof. unfold fsupp, seq; desf; ins; desf. specialize (FS2 y); desf. apply fsupp_list with (l:=findom) in FS1; desf. exists findom0; ins; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom