proposition: Lemma fsupp_cr r : fsupp r -> fsupp r^?.
proof: Proof. rewrite crE; ins; eauto using fsupp_eqv, fsupp_union. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom